diff --git a/CMakeLists.txt b/CMakeLists.txt index 9f6a50f70..76d554806 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -132,7 +132,7 @@ else(CLANG) endif() add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE) - set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-newline-eof -Wno-mismatched-tags -Wno-unused-local-typedefs -ftemplate-depth=1024") + set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-newline-eof -Wno-mismatched-tags -Wno-unused-local-typedefs -ftemplate-depth=1024 -Wno-parentheses-equality") if(FORCE_COLOR) set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fcolor-diagnostics") @@ -188,7 +188,7 @@ if(CUSTOM_BOOST_ROOT) set(BOOST_ROOT "${CUSTOM_BOOST_ROOT}") endif(CUSTOM_BOOST_ROOT) -find_package(Boost REQUIRED) +find_package(Boost 1.56.0 REQUIRED) if ((NOT Boost_LIBRARY_DIRS) OR ("${Boost_LIBRARY_DIRS}" STREQUAL "")) set(Boost_LIBRARY_DIRS "${Boost_INCLUDE_DIRS}/stage/lib") diff --git a/resources/3rdparty/cudd-2.5.0/CMakeLists.txt b/resources/3rdparty/cudd-2.5.0/CMakeLists.txt index 4a39bd5da..5df298c34 100644 --- a/resources/3rdparty/cudd-2.5.0/CMakeLists.txt +++ b/resources/3rdparty/cudd-2.5.0/CMakeLists.txt @@ -26,7 +26,7 @@ elseif(MSVC) # required for GMM to compile, ugly error directive in their code add_definitions(/D_SCL_SECURE_NO_DEPRECATE /D_CRT_SECURE_NO_WARNINGS) else(CLANG) - set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-newline-eof -Wno-unneeded-internal-declaration -Wno-unused-variable -Wno-unused-const-variable") + set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-newline-eof -Wno-unneeded-internal-declaration -Wno-unused-variable -Wno-unused-const-variable -Wno-parentheses-equality") endif() # Since we do not target Alphas, this symbol is always set diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index ed0f43d3b..d345d9f05 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -264,7 +264,7 @@ 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 the set of labels we are supposed to built is restricted, we need to remove the other labels from the program. if (options.labelsToBuild) { if (!options.buildAllLabels) { diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 0909b25de..758ac9a2a 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -236,15 +236,15 @@ namespace storm { if (settings.isSymbolicSet()) { #ifdef STORM_HAVE_CARL if (settings.isParametricSet()) { - buildAndCheckSymbolicModel(program.get(), formulas); + buildAndCheckSymbolicModel(program.get(), formulas, true); } else { #endif - buildAndCheckSymbolicModel(program.get(), formulas); + buildAndCheckSymbolicModel(program.get(), formulas, true); #ifdef STORM_HAVE_CARL } #endif } else if (settings.isExplicitSet()) { - buildAndCheckExplicitModel(formulas); + buildAndCheckExplicitModel(formulas, true); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index cddebdf7f..bbb9d6404 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -9,10 +9,10 @@ namespace storm { namespace cli { template - void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas) { + void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { for (auto const& formula : formulas) { std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result(storm::verifySparseModel(model, formula)); + std::unique_ptr result(storm::verifySparseModel(model, formula, onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; @@ -26,12 +26,12 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - inline void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas) { + inline void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant) { for (auto const& formula : formulas) { STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs."); std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result(storm::verifySparseModel(model, formula)); + std::unique_ptr result(storm::verifySparseModel(model, formula, onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; @@ -50,15 +50,15 @@ namespace storm { #endif template - void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector> const& formulas) { + void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented."); } template - void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector> const& formulas) { + void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { for (auto const& formula : formulas) { std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result(storm::verifySymbolicModelWithHybridEngine(model, formula)); + std::unique_ptr result(storm::verifySymbolicModelWithHybridEngine(model, formula, onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; @@ -72,10 +72,10 @@ namespace storm { } template - void verifySymbolicModelWithSymbolicEngine(std::shared_ptr> model, std::vector> const& formulas) { + void verifySymbolicModelWithSymbolicEngine(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { for (auto const& formula : formulas) { std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result(storm::verifySymbolicModelWithDdEngine(model, formula)); + std::unique_ptr result(storm::verifySymbolicModelWithDdEngine(model, formula, onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; @@ -114,12 +114,12 @@ namespace storm { } template - void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { + void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement) { - verifySymbolicModelWithAbstractionRefinementEngine(program, formulas); + verifySymbolicModelWithAbstractionRefinementEngine(program, formulas, onlyInitialStatesRelevant); } else { storm::storage::ModelFormulasPair modelFormulasPair = buildSymbolicModel(program, formulas); STORM_LOG_THROW(modelFormulasPair.model != nullptr, storm::exceptions::InvalidStateException, @@ -133,7 +133,6 @@ namespace storm { // Verify the model, if a formula was given. if (!formulas.empty()) { - if (modelFormulasPair.model->isSparseModel()) { if (storm::settings::generalSettings().isCounterexampleSet()) { // If we were requested to generate a counterexample, we now do so for each formula. @@ -141,15 +140,15 @@ namespace storm { generateCounterexample(program, modelFormulasPair.model->as>(), formula); } } else { - verifySparseModel(modelFormulasPair.model->as>(), modelFormulasPair.formulas); + verifySparseModel(modelFormulasPair.model->as>(), modelFormulasPair.formulas, onlyInitialStatesRelevant); } } else if (modelFormulasPair.model->isSymbolicModel()) { if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { verifySymbolicModelWithHybridEngine(modelFormulasPair.model->as>(), - modelFormulasPair.formulas); + modelFormulasPair.formulas, onlyInitialStatesRelevant); } else { verifySymbolicModelWithSymbolicEngine(modelFormulasPair.model->as>(), - modelFormulasPair.formulas); + modelFormulasPair.formulas, onlyInitialStatesRelevant); } } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); @@ -159,20 +158,20 @@ namespace storm { } template - void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { + void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::CUDD) { - buildAndCheckSymbolicModel(program, formulas); + buildAndCheckSymbolicModel(program, formulas, onlyInitialStatesRelevant); } else if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::Sylvan) { - buildAndCheckSymbolicModel(program, formulas); + buildAndCheckSymbolicModel(program, formulas, onlyInitialStatesRelevant); } } template - void buildAndCheckExplicitModel(std::vector> const& formulas) { + void buildAndCheckExplicitModel(std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); - std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional(), settings.isChoiceLabelingSet() ? settings.getChoiceLabelingFilename() : boost::optional()); + std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional(settings.getChoiceLabelingFilename()) : boost::none); // Preprocess the model if needed. BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulas); @@ -183,7 +182,7 @@ namespace storm { // Verify the model, if a formula was given. if (!formulas.empty()) { STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); - verifySparseModel(model->as>(), formulas); + verifySparseModel(model->as>(), formulas, onlyInitialStatesRelevant); } } } 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/logic/Formula.cpp b/src/logic/Formula.cpp index babf9edfc..5ba068af9 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -115,6 +115,10 @@ namespace storm { return false; } + bool Formula::isOperatorFormula() const { + return false; + } + bool Formula::isPctlPathFormula() const { return false; } @@ -379,6 +383,14 @@ namespace storm { return dynamic_cast(*this); } + OperatorFormula& Formula::asOperatorFormula() { + return dynamic_cast(*this); + } + + OperatorFormula const& Formula::asOperatorFormula() const { + return dynamic_cast(*this); + } + std::vector> Formula::getAtomicExpressionFormulas() const { std::vector> result; this->gatherAtomicExpressionFormulas(result); diff --git a/src/logic/Formula.h b/src/logic/Formula.h index 1a6933703..31ee7744a 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -38,6 +38,7 @@ namespace storm { class LongRunAverageRewardFormula; class ProbabilityOperatorFormula; class RewardOperatorFormula; + class OperatorFormula; // Also foward-declare base model checker class. class ModelChecker; @@ -80,6 +81,7 @@ namespace storm { virtual bool isLongRunAverageRewardFormula() const; virtual bool isProbabilityOperatorFormula() const; virtual bool isRewardOperatorFormula() const; + virtual bool isOperatorFormula() const; virtual bool isPctlPathFormula() const; virtual bool isPctlStateFormula() const; @@ -175,6 +177,9 @@ namespace storm { RewardOperatorFormula& asRewardOperatorFormula(); RewardOperatorFormula const& asRewardOperatorFormula() const; + OperatorFormula& asOperatorFormula(); + OperatorFormula const& asOperatorFormula() const; + std::vector> getAtomicExpressionFormulas() const; std::vector> getAtomicLabelFormulas() const; std::set getReferencedRewardModels() const; diff --git a/src/logic/Formulas.h b/src/logic/Formulas.h index faf4ca164..3671b2859 100644 --- a/src/logic/Formulas.h +++ b/src/logic/Formulas.h @@ -13,6 +13,7 @@ #include "src/logic/NextFormula.h" #include "src/logic/PathFormula.h" #include "src/logic/RewardPathFormula.h" +#include "src/logic/OperatorFormula.h" #include "src/logic/ProbabilityOperatorFormula.h" #include "src/logic/ReachabilityRewardFormula.h" #include "src/logic/LongRunAverageRewardFormula.h" diff --git a/src/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp index 39fad071d..768b6b3d0 100644 --- a/src/logic/OperatorFormula.cpp +++ b/src/logic/OperatorFormula.cpp @@ -34,6 +34,10 @@ namespace storm { return optimalityType.get(); } + bool OperatorFormula::isOperatorFormula() const { + return true; + } + std::ostream& OperatorFormula::writeToStream(std::ostream& out) const { if (hasOptimalityType()) { out << (getOptimalityType() == OptimizationDirection::Minimize ? "min" : "max"); diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h index a059ddb8b..5c120bf2f 100644 --- a/src/logic/OperatorFormula.h +++ b/src/logic/OperatorFormula.h @@ -24,6 +24,7 @@ namespace storm { void setBound(double); bool hasOptimalityType() const; OptimizationDirection const& getOptimalityType() const; + virtual bool isOperatorFormula() const override; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 2b840d83c..764b02427 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -11,137 +11,144 @@ namespace storm { namespace modelchecker { - std::unique_ptr AbstractModelChecker::check(storm::logic::Formula const& formula) { + 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 << "'."); if (formula.isStateFormula()) { - return this->checkStateFormula(formula.asStateFormula()); + return this->checkStateFormula(checkTask.replaceFormula(formula.asStateFormula())); } else if (formula.isPathFormula()) { - return this->computeProbabilities(formula.asPathFormula()); + return this->computeProbabilities(checkTask.replaceFormula(formula.asPathFormula())); } else if (formula.isRewardPathFormula()) { - return this->computeRewards(formula.asRewardPathFormula()); + 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, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeProbabilities(CheckTask const& checkTask) { + storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); if (pathFormula.isBoundedUntilFormula()) { - return this->computeBoundedUntilProbabilities(pathFormula.asBoundedUntilFormula(), qualitative, optimalityType); + return this->computeBoundedUntilProbabilities(checkTask.replaceFormula(pathFormula.asBoundedUntilFormula())); } else if (pathFormula.isConditionalPathFormula()) { - return this->computeConditionalProbabilities(pathFormula.asConditionalPathFormula(), qualitative, optimalityType); + return this->computeConditionalProbabilities(checkTask.replaceFormula(pathFormula.asConditionalPathFormula())); } else if (pathFormula.isEventuallyFormula()) { - return this->computeEventuallyProbabilities(pathFormula.asEventuallyFormula(), qualitative, optimalityType); + return this->computeEventuallyProbabilities(checkTask.replaceFormula(pathFormula.asEventuallyFormula())); } else if (pathFormula.isGloballyFormula()) { - return this->computeGloballyProbabilities(pathFormula.asGloballyFormula(), qualitative, optimalityType); + return this->computeGloballyProbabilities(checkTask.replaceFormula(pathFormula.asGloballyFormula())); } else if (pathFormula.isUntilFormula()) { - return this->computeUntilProbabilities(pathFormula.asUntilFormula(), qualitative, optimalityType); + return this->computeUntilProbabilities(checkTask.replaceFormula(pathFormula.asUntilFormula())); } else if (pathFormula.isNextFormula()) { - return this->computeNextProbabilities(pathFormula.asNextFormula(), qualitative, optimalityType); + 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, bool qualitative, boost::optional const& optimalityType) { - 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, bool qualitative, boost::optional const& optimalityType) { - 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, bool qualitative, boost::optional const& optimalityType) { + 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, qualitative, optimalityType); + return this->computeUntilProbabilities(checkTask.replaceFormula(newFormula)); } - std::unique_ptr AbstractModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - 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, bool qualitative, boost::optional const& optimalityType) { - 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, bool qualitative, boost::optional const& optimalityType) { - 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 const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr AbstractModelChecker::computeRewards(CheckTask const& checkTask) { + storm::logic::RewardPathFormula const& rewardPathFormula = checkTask.getFormula(); if (rewardPathFormula.isCumulativeRewardFormula()) { - return this->computeCumulativeRewards(rewardPathFormula.asCumulativeRewardFormula(), rewardModelName, qualitative, optimalityType); + return this->computeCumulativeRewards(checkTask.replaceFormula(rewardPathFormula.asCumulativeRewardFormula())); } else if (rewardPathFormula.isInstantaneousRewardFormula()) { - return this->computeInstantaneousRewards(rewardPathFormula.asInstantaneousRewardFormula(), rewardModelName, qualitative, optimalityType); + return this->computeInstantaneousRewards(checkTask.replaceFormula(rewardPathFormula.asInstantaneousRewardFormula())); } else if (rewardPathFormula.isReachabilityRewardFormula()) { - return this->computeReachabilityRewards(rewardPathFormula.asReachabilityRewardFormula(), rewardModelName, qualitative, optimalityType); + return this->computeReachabilityRewards(checkTask.replaceFormula(rewardPathFormula.asReachabilityRewardFormula())); } else if (rewardPathFormula.isLongRunAverageRewardFormula()) { - return this->computeLongRunAverageRewards(rewardPathFormula.asLongRunAverageRewardFormula(), rewardModelName, qualitative, optimalityType); + 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 const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - 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 const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - 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 const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - 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 const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - 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, bool qualitative, boost::optional const& optimalityType) { - 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, bool qualitative, boost::optional const& optimalityType) { - 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) { + std::unique_ptr AbstractModelChecker::checkStateFormula(CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); if (stateFormula.isBinaryBooleanStateFormula()) { - return this->checkBinaryBooleanStateFormula(stateFormula.asBinaryBooleanStateFormula()); + return this->checkBinaryBooleanStateFormula(checkTask.replaceFormula(stateFormula.asBinaryBooleanStateFormula())); } else if (stateFormula.isUnaryBooleanStateFormula()) { - return this->checkUnaryBooleanStateFormula(stateFormula.asUnaryBooleanStateFormula()); + return this->checkUnaryBooleanStateFormula(checkTask.replaceFormula(stateFormula.asUnaryBooleanStateFormula())); } else if (stateFormula.isBooleanLiteralFormula()) { - return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula()); + return this->checkBooleanLiteralFormula(checkTask.replaceFormula(stateFormula.asBooleanLiteralFormula())); } else if (stateFormula.isProbabilityOperatorFormula()) { - return this->checkProbabilityOperatorFormula(stateFormula.asProbabilityOperatorFormula()); + return this->checkProbabilityOperatorFormula(checkTask.replaceFormula(stateFormula.asProbabilityOperatorFormula())); } else if (stateFormula.isRewardOperatorFormula()) { - return this->checkRewardOperatorFormula(stateFormula.asRewardOperatorFormula()); + return this->checkRewardOperatorFormula(checkTask.replaceFormula(stateFormula.asRewardOperatorFormula())); } else if (stateFormula.isExpectedTimeOperatorFormula()) { - return this->checkExpectedTimeOperatorFormula(stateFormula.asExpectedTimeOperatorFormula()); + return this->checkExpectedTimeOperatorFormula(checkTask.replaceFormula(stateFormula.asExpectedTimeOperatorFormula())); } else if (stateFormula.isLongRunAverageOperatorFormula()) { - return this->checkLongRunAverageOperatorFormula(stateFormula.asLongRunAverageOperatorFormula()); + return this->checkLongRunAverageOperatorFormula(checkTask.replaceFormula(stateFormula.asLongRunAverageOperatorFormula())); } else if (stateFormula.isAtomicExpressionFormula()) { - return this->checkAtomicExpressionFormula(stateFormula.asAtomicExpressionFormula()); + return this->checkAtomicExpressionFormula(checkTask.replaceFormula(stateFormula.asAtomicExpressionFormula())); } else if (stateFormula.isAtomicLabelFormula()) { - return this->checkAtomicLabelFormula(stateFormula.asAtomicLabelFormula()); + return this->checkAtomicLabelFormula(checkTask.replaceFormula(stateFormula.asAtomicLabelFormula())); } else if (stateFormula.isBooleanLiteralFormula()) { - return this->checkBooleanLiteralFormula(stateFormula.asBooleanLiteralFormula()); + 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) { + 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())); + return this->checkAtomicLabelFormula(checkTask.replaceFormula(storm::logic::AtomicLabelFormula(stream.str()))); } - std::unique_ptr AbstractModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { - 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) { + 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."); @@ -156,33 +163,15 @@ namespace storm { return leftResult; } - std::unique_ptr AbstractModelChecker::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) { - 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) { + 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."); - // 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."); @@ -192,95 +181,51 @@ namespace storm { } } - std::unique_ptr AbstractModelChecker::checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula) { + 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) { + 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) { + 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) { - 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 5fca10010..a4ad1b6ac 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -3,6 +3,7 @@ #include +#include "src/modelchecker/CheckTask.h" #include "src/logic/Formulas.h" #include "src/solver/OptimizationDirection.h" @@ -17,53 +18,53 @@ namespace storm { } /*! - * Determines whether the model checker can handle the formula. If this method returns false, the formula - * must not be checked using the model checker. + * Determines whether the model checker can handle the given verification task. If this method returns + * false, the task must not be checked using this model checker. * - * @param formula The formula for which to check whether the model checker can handle it. - * @return True iff the model checker can check the given formula. + * @param checkTask The task for which to check whether the model checker can handle it. + * @return True iff the model checker can check the given task. */ - virtual bool canHandle(storm::logic::Formula const& formula) const = 0; + virtual bool canHandle(CheckTask const& checkTask) const = 0; /*! * Checks the provided formula. * - * @param formula The formula to check. + * @param checkTask The verification task to pursue. * @return The verification result. */ - virtual std::unique_ptr check(storm::logic::Formula const& formula); + 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, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + 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 const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + 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, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); - virtual std::unique_ptr computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()); + 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); - virtual std::unique_ptr checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula); - virtual std::unique_ptr checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula); - virtual std::unique_ptr checkBinaryBooleanStateFormula(storm::logic::BinaryBooleanStateFormula const& stateFormula); - virtual std::unique_ptr checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula); - virtual std::unique_ptr checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula); - virtual std::unique_ptr checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula); - virtual std::unique_ptr checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula); - virtual std::unique_ptr checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula); - virtual std::unique_ptr checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula); + 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.h b/src/modelchecker/CheckTask.h new file mode 100644 index 000000000..cf66f4f06 --- /dev/null +++ b/src/modelchecker/CheckTask.h @@ -0,0 +1,221 @@ +#ifndef STORM_MODELCHECKER_CHECKTASK_H_ +#define STORM_MODELCHECKER_CHECKTASK_H_ + +#include + +#include "src/logic/Formulas.h" +#include "src/utility/constants.h" + +#include "src/solver/OptimizationDirection.h" +#include "src/logic/ComparisonType.h" + +namespace storm { + namespace logic { + class Formula; + } + + namespace modelchecker { + + /* + * This class is used to customize the checking process of a formula. + */ + template + class CheckTask { + public: + template + friend class CheckTask; + + /*! + * Creates a task object with the default options for the given formula. + */ + CheckTask(FormulaType const& formula, bool onlyInitialStatesRelevant = false) : formula(formula) { + this->onlyInitialStatesRelevant = onlyInitialStatesRelevant; + this->produceStrategies = true; + this->qualitative = false; + + if (formula.isOperatorFormula()) { + storm::logic::OperatorFormula const& operatorFormula = formula.asOperatorFormula(); + if (operatorFormula.hasOptimalityType()) { + this->optimizationDirection = operatorFormula.getOptimalityType(); + } + + if (operatorFormula.hasBound()) { + if (onlyInitialStatesRelevant) { + this->bound = std::make_pair(operatorFormula.getComparisonType(), static_cast(operatorFormula.getBound())); + } + + if (!optimizationDirection) { + this->optimizationDirection = operatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || operatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; + } + } + } + + if (formula.isProbabilityOperatorFormula()) { + storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); + + if (probabilityOperatorFormula.hasBound()) { + if (probabilityOperatorFormula.getBound() == storm::utility::zero() || probabilityOperatorFormula.getBound() == storm::utility::one()) { + this->qualitative = true; + } + } + } else if (formula.isRewardOperatorFormula()) { + storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula(); + this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName(); + + if (rewardOperatorFormula.hasBound()) { + if (rewardOperatorFormula.getBound() == storm::utility::zero()) { + this->qualitative = true; + } + } + } + } + + /*! + * 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 replaceFormula(NewFormulaType const& newFormula) const { + return CheckTask(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceStrategies); + } + + /*! + * Retrieves the formula from this task. + */ + FormulaType const& getFormula() const { + return formula.get(); + } + + /*! + * Retrieves whether an optimization direction was set. + */ + bool isOptimizationDirectionSet() const { + return static_cast(optimizationDirection); + } + + /*! + * Retrieves the optimization direction (if set). + */ + storm::OptimizationDirection const& getOptimizationDirection() const { + return optimizationDirection.get(); + } + + /*! + * Retrieves whether a reward model was set. + */ + bool isRewardModelSet() const { + return static_cast(rewardModel); + } + + /*! + * Retrieves the reward model over which to perform the checking (if set). + */ + std::string const& getRewardModel() const { + return rewardModel.get(); + } + + /*! + * Retrieves whether only the initial states are relevant in the computation. + */ + bool isOnlyInitialStatesRelevantSet() const { + return onlyInitialStatesRelevant; + } + + /*! + * Sets whether only initial states are relevant. + */ + CheckTask& setOnlyInitialStatesRelevant(bool value = true) { + this->onlyInitialStatesRelevant = value; + return *this; + } + + /*! + * 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 the comparison type of the bound (if set). + */ + storm::logic::ComparisonType const& getBoundComparisonType() const { + return bound.get().first; + } + + /*! + * Retrieves the bound for the initial states (if set). + */ + 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 { + return qualitative; + } + + /*! + * Retrieves whether strategies are to be produced (if supported). + */ + bool isProduceStrategiesSet() const { + return produceStrategies; + } + + private: + /*! + * 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 + * for the initial states. + * @param initialStatesBound The bound with which the initial states will be compared. This may only be set + * together with the flag that indicates only initial states of the model are relevant. + * @param qualitative A flag specifying whether the property needs to be checked qualitatively, i.e. compared + * with bounds 0/1. + * @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(std::reference_wrapper 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. + std::reference_wrapper formula; + + // If set, the probabilities will be minimized/maximized. + boost::optional optimizationDirection; + + // If set, the reward property has to be interpreted over this model. + boost::optional rewardModel; + + // If set to true, the model checker may decide to only compute the values for the initial states. + bool onlyInitialStatesRelevant; + + // The bound with which the initial states will be compared. + boost::optional> bound; + + // A flag specifying whether the property needs to be checked qualitatively, i.e. compared with bounds 0/1. + bool qualitative; + + // If supported by the model checker and the model formalism, strategies to achieve a value will be produced + // if this flag is set. + bool produceStrategies; + }; + + } +} + +#endif /* STORM_MODELCHECKER_CHECKTASK_H_ */ \ No newline at end of file diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 42c9466d1..a5eb27b27 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -23,22 +23,25 @@ namespace storm { } template - bool HybridCtmcCslModelChecker::canHandle(storm::logic::Formula const& formula) const { + bool HybridCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isCslStateFormula() || formula.isCslPathFormula() || formula.isRewardPathFormula(); } template - std::unique_ptr HybridCtmcCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridCtmcCslModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridCtmcCslModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridCtmcCslModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -51,15 +54,17 @@ namespace storm { } template - std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridCtmcCslModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); } template - std::unique_ptr HybridCtmcCslModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridCtmcCslModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); @@ -74,25 +79,28 @@ namespace storm { upperBound = pathFormula.getDiscreteTimeBound(); } - return storm::modelchecker::helper::HybridCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, lowerBound, upperBound, *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), lowerBound, upperBound, *linearEquationSolverFactory); } template - std::unique_ptr HybridCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - return storm::modelchecker::helper::HybridCtmcCslHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); + std::unique_ptr HybridCtmcCslModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); } template - std::unique_ptr HybridCtmcCslModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); + std::unique_ptr HybridCtmcCslModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { + storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); } template - std::unique_ptr HybridCtmcCslModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridCtmcCslModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); } // Explicitly instantiate the model checker. diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/modelchecker/csl/HybridCtmcCslModelChecker.h index ed4125c7e..ace5b420b 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.h +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.h @@ -17,14 +17,14 @@ namespace storm { explicit HybridCtmcCslModelChecker(storm::models::symbolic::Ctmc const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; protected: storm::models::symbolic::Ctmc const& getModel() const override; diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 3648f8bb4..b06cc2a54 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -30,12 +30,14 @@ namespace storm { } template - bool SparseCtmcCslModelChecker::canHandle(storm::logic::Formula const& formula) const { + bool SparseCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isCslStateFormula() || formula.isCslPathFormula() || formula.isRewardPathFormula(); } template - std::unique_ptr SparseCtmcCslModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseCtmcCslModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();; @@ -50,12 +52,13 @@ namespace storm { upperBound = pathFormula.getDiscreteTimeBound(); } - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), qualitative, lowerBound, upperBound, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), checkTask.isQualitativeSet(), lowerBound, upperBound, *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseCtmcCslModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseCtmcCslModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeNextProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), *linearEquationSolverFactory); @@ -63,43 +66,48 @@ namespace storm { } template - std::unique_ptr SparseCtmcCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseCtmcCslModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); + std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); + std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { + storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getContinuousTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); storm::storage::SparseMatrix probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h index 78e2fd91f..d4e36071a 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -20,14 +20,14 @@ namespace storm { explicit SparseCtmcCslModelChecker(SparseCtmcModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; private: // An object that is used for solving linear equations and performing matrix-vector multiplication. diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index b93643d62..b33b01436 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -28,64 +28,70 @@ namespace storm { } template - bool SparseMarkovAutomatonCslModelChecker::canHandle(storm::logic::Formula const& formula) const { + bool SparseMarkovAutomatonCslModelChecker::canHandle(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isCslStateFormula() || formula.isCslPathFormula() || (formula.isRewardPathFormula() && formula.isReachabilityRewardFormula()); } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(pathFormula.getLeftSubformula().isTrueFormula(), storm::exceptions::NotImplementedException, "Only bounded properties of the form 'true U[t1, t2] phi' are currently supported."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute time-bounded reachability probabilities in non-closed Markov automaton."); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds(), *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute reachability rewards in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute long-run average in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } template - std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeExpectedTimes(CheckTask const& checkTask) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute expected times in non-closed Markov automaton."); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeExpectedTimes(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeExpectedTimes(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index a3d0fc1fb..e57f9d3e5 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -20,12 +20,12 @@ namespace storm { explicit SparseMarkovAutomatonCslModelChecker(SparseMarkovAutomatonModelType const& model); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeExpectedTimes(CheckTask const& checkTask) override; private: // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices. diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 6614bf8e7..c5e2225aa 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -34,35 +34,40 @@ namespace storm { } template - bool HybridDtmcPrctlModelChecker::canHandle(storm::logic::Formula const& formula) const { + bool HybridDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula(); } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -72,22 +77,25 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { + storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template @@ -96,7 +104,8 @@ namespace storm { } template - std::unique_ptr HybridDtmcPrctlModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr HybridDtmcPrctlModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); @@ -105,7 +114,7 @@ namespace storm { storm::storage::SparseMatrix explicitProbabilityMatrix = this->getModel().getTransitionMatrix().toMatrix(odd, odd); - std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, subResult.getTruthValuesVector().toVector(odd), qualitative, *this->linearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, subResult.getTruthValuesVector().toVector(odd), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().template getAddZero(), this->getModel().getReachableStates(), std::move(odd), std::move(result))); } diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index 5d68a8785..4d64f6f17 100644 --- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -17,15 +17,15 @@ namespace storm { explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; protected: storm::models::symbolic::Dtmc const& getModel() const override; diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index f7b44adcb..6dfd0d83b 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -28,12 +28,13 @@ namespace storm { } template - bool HybridMdpPrctlModelChecker::canHandle(storm::logic::Formula const& formula) const { + bool HybridMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { return true; } if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(formula.asProbabilityOperatorFormula().getSubformula()); + return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula())); } if (formula.isGloballyFormula()) { return true; @@ -42,62 +43,69 @@ namespace storm { } template - std::unique_ptr HybridMdpPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr HybridMdpPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeUntilProbabilities(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridMdpPrctlModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr HybridMdpPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeGloballyProbabilities(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeGloballyProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridMdpPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr HybridMdpPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeNextProbabilities(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeNextProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); } template - std::unique_ptr HybridMdpPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr HybridMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr HybridMdpPrctlModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { + storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeCumulativeRewards(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr HybridMdpPrctlModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeInstantaneousRewards(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr HybridMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr HybridMdpPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeReachabilityRewards(optimalityType.get(), this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h index 4cd1d6e27..78612a378 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -24,14 +24,14 @@ namespace storm { explicit HybridMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; protected: storm::models::symbolic::Mdp const& getModel() const override; diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 5103fc3a0..d4bb73950 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -32,7 +32,8 @@ namespace storm { } template - bool SparseDtmcPrctlModelChecker::canHandle(storm::logic::Formula const& formula) const { + bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { return true; } @@ -40,7 +41,7 @@ namespace storm { return true; } if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(formula.asProbabilityOperatorFormula().getSubformula()); + return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula())); } if (formula.isConditionalPathFormula()) { storm::logic::ConditionalPathFormula const& conditionalPathFormula = formula.asConditionalPathFormula(); @@ -52,7 +53,8 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -64,7 +66,8 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeNextProbabilities(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *linearEquationSolverFactory); @@ -72,55 +75,62 @@ namespace storm { } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeGloballyProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeGloballyProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { + storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative , boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { + storm::logic::ConditionalPathFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); @@ -129,7 +139,7 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 384130263..77217a3ac 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -19,16 +19,16 @@ namespace storm { explicit SparseDtmcPrctlModelChecker(SparseDtmcModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; private: // An object that is used for retrieving linear equation solvers. diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index eabe827f3..eb4025551 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -37,12 +37,13 @@ namespace storm { } template - bool SparseMdpPrctlModelChecker::canHandle(storm::logic::Formula const& formula) const { + bool SparseMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { return true; } if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(formula.asProbabilityOperatorFormula().getSubformula()); + return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula())); } if (formula.isGloballyFormula()) { return true; @@ -57,48 +58,53 @@ namespace storm { } template - std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SparseMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseMdpPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SparseMdpPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeNextProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseMdpPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SparseMdpPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, false, *minMaxLinearEquationSolverFactory); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), false, *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret.result))); } template - std::unique_ptr SparseMdpPrctlModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SparseMdpPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret))); } template - std::unique_ptr SparseMdpPrctlModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SparseMdpPrctlModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { + storm::logic::ConditionalPathFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidPropertyException, "Cannot compute conditional probabilities on MDPs with more than one initial state."); STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); @@ -108,60 +114,44 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - return storm::modelchecker::helper::SparseMdpPrctlHelper::computeConditionalProbabilities(optimalityType.get(), *this->getModel().getInitialStates().begin(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + return storm::modelchecker::helper::SparseMdpPrctlHelper::computeConditionalProbabilities(checkTask.getOptimizationDirection(), *this->getModel().getInitialStates().begin(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); } template - std::unique_ptr SparseMdpPrctlModelChecker::computeUntilProbabilitiesForInitialStates(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType, boost::optional> const& bound) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); - std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); - std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); - ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); - ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - if(qualitative | !bound) { - // For qualitative checks, or if the , we use the standard approach. - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, false, *minMaxLinearEquationSolverFactory); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret.result))); - } else { - // With a given bound, we only iterate until we pass the bound. - storm::solver::BoundedGoal boundedGoal(optimalityType.get(), bound.get(), this->getModel().getInitialStates() ); - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(boundedGoal, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, false, *minMaxLinearEquationSolverFactory); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret.result))); - } - - } - - template - std::unique_ptr SparseMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SparseMdpPrctlModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { + storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(optimalityType.get(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SparseMdpPrctlModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeInstantaneousRewards(optimalityType.get(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SparseMdpPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityRewards(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template - std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverageProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index d36bdcec1..340b5f33a 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,24 +15,20 @@ 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); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilitiesForInitialStates(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional(), boost::optional> const& bound =boost::optional>()); - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; private: // An object that is used for retrieving solvers for systems of linear equations that are the result of nondeterministic choices. diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 920102389..0053d6b77 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -30,12 +30,13 @@ namespace storm { } template - bool SymbolicDtmcPrctlModelChecker::canHandle(storm::logic::Formula const& formula) const { + bool SymbolicDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { return true; } if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(formula.asProbabilityOperatorFormula().getSubformula()); + return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula())); } if (formula.isGloballyFormula()) { return true; @@ -44,25 +45,28 @@ namespace storm { } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); @@ -70,7 +74,8 @@ namespace storm { } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -81,24 +86,27 @@ namespace storm { } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { + storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } template - std::unique_ptr SymbolicDtmcPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SymbolicDtmcPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h index 8c8d4140d..a7968a56a 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h @@ -14,14 +14,14 @@ namespace storm { explicit SymbolicDtmcPrctlModelChecker(storm::models::symbolic::Dtmc const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; protected: storm::models::symbolic::Dtmc const& getModel() const override; diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 296236f07..30891afdf 100644 --- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -30,12 +30,13 @@ namespace storm { } template - bool SymbolicMdpPrctlModelChecker::canHandle(storm::logic::Formula const& formula) const { + bool SymbolicMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) { return true; } if (formula.isProbabilityOperatorFormula()) { - return this->canHandle(formula.asProbabilityOperatorFormula().getSubformula()); + return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula())); } if (formula.isGloballyFormula()) { return true; @@ -44,62 +45,69 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SymbolicMdpPrctlModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SymbolicMdpPrctlModelChecker::computeGloballyProbabilities(CheckTask const& checkTask) { + storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeGloballyProbabilities(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeGloballyProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SymbolicMdpPrctlModelChecker::computeNextProbabilities(CheckTask const& checkTask) { + storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeNextProbabilities(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeNextProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SymbolicMdpPrctlModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SymbolicMdpPrctlModelChecker::computeCumulativeRewards(CheckTask const& checkTask) { + storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeCumulativeRewards(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SymbolicMdpPrctlModelChecker::computeInstantaneousRewards(CheckTask const& checkTask) { + storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeInstantaneousRewards(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template - std::unique_ptr SymbolicMdpPrctlModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + std::unique_ptr SymbolicMdpPrctlModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(optimalityType.get() == OptimizationDirection::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template diff --git a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h index e5160faa8..1baca69da 100644 --- a/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h @@ -16,14 +16,14 @@ namespace storm { explicit SymbolicMdpPrctlModelChecker(storm::models::symbolic::Mdp const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; protected: storm::models::symbolic::Mdp const& getModel() const override; diff --git a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index 17705fdbb..52447c289 100644 --- a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -23,11 +23,11 @@ namespace storm { namespace helper { template - std::unique_ptr SymbolicMdpPrctlHelper::computeUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr SymbolicMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 and 1 of satisfying the until-formula. std::pair, storm::dd::Bdd> statesWithProbability01; - if (minimize) { + if (dir == OptimizationDirection::Minimize) { statesWithProbability01 = storm::utility::graph::performProb01Min(model, phiStates, psiStates); } else { statesWithProbability01 = storm::utility::graph::performProb01Max(model, phiStates, psiStates); @@ -66,7 +66,7 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->solveEquationSystem(minimize, model.getManager().template getAddZero(), subvector); + storm::dd::Add result = solver->solveEquationSystem(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), subvector); return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), statesWithProbability01.second.template toAdd() + result)); } else { @@ -76,24 +76,24 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlHelper::computeGloballyProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { - std::unique_ptr result = computeUntilProbabilities(!minimize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); + std::unique_ptr SymbolicMdpPrctlHelper::computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); result->asQuantitativeCheckResult().oneMinus(); return result; } template - std::unique_ptr SymbolicMdpPrctlHelper::computeNextProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates) { + std::unique_ptr SymbolicMdpPrctlHelper::computeNextProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates) { storm::dd::Add result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd(); return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result.sumAbstract(model.getColumnVariables()))); } template - std::unique_ptr SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 or 1 of satisfying the until-formula. storm::dd::Bdd statesWithProbabilityGreater0; - if (minimize) { + if (dir == OptimizationDirection::Minimize) { statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0A(model, transitionMatrix.notZero(), phiStates, psiStates); } else { statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(model, transitionMatrix.notZero(), phiStates, psiStates); @@ -118,7 +118,7 @@ namespace storm { submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->performMatrixVectorMultiplication(minimize, model.getManager().template getAddZero(), &subvector, stepBound); + storm::dd::Add result = solver->performMatrixVectorMultiplication(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), &subvector, stepBound); return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.template toAdd() + result)); } else { @@ -127,19 +127,19 @@ namespace storm { } template - std::unique_ptr SymbolicMdpPrctlHelper::computeInstantaneousRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr SymbolicMdpPrctlHelper::computeInstantaneousRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(model.getTransitionMatrix(), model.getReachableStates(), model.getIllegalMask(), model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->performMatrixVectorMultiplication(minimize, rewardModel.getStateRewardVector(), nullptr, stepBound); + storm::dd::Add result = solver->performMatrixVectorMultiplication(dir == OptimizationDirection::Minimize, rewardModel.getStateRewardVector(), nullptr, stepBound); return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result)); } template - std::unique_ptr SymbolicMdpPrctlHelper::computeCumulativeRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr SymbolicMdpPrctlHelper::computeCumulativeRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -148,13 +148,13 @@ namespace storm { // Perform the matrix-vector multiplication. std::unique_ptr> solver = linearEquationSolverFactory.create(model.getTransitionMatrix(), model.getReachableStates(), model.getIllegalMask(), model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->performMatrixVectorMultiplication(minimize, model.getManager().template getAddZero(), &totalRewardVector, stepBound); + storm::dd::Add result = solver->performMatrixVectorMultiplication(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), &totalRewardVector, stepBound); return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result)); } template - std::unique_ptr SymbolicMdpPrctlHelper::computeReachabilityRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr SymbolicMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if there is at least one reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -162,7 +162,7 @@ namespace storm { // Determine which states have a reward of infinity by definition. storm::dd::Bdd infinityStates; storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); - if (minimize) { + if (dir == OptimizationDirection::Minimize) { infinityStates = storm::utility::graph::performProb1E(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0E(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); } else { infinityStates = storm::utility::graph::performProb1A(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0A(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); @@ -197,7 +197,7 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->solveEquationSystem(minimize, model.getManager().template getAddZero(), subvector); + storm::dd::Add result = solver->solveEquationSystem(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), subvector); return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), result))); } else { diff --git a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h index 25b01d449..083840a00 100644 --- a/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h @@ -7,6 +7,7 @@ #include "src/storage/dd/Bdd.h" #include "src/utility/solver.h" +#include "src/solver/SolveGoal.h" namespace storm { namespace modelchecker { @@ -20,19 +21,19 @@ namespace storm { public: typedef typename storm::models::symbolic::NondeterministicModel::RewardModelType RewardModelType; - static std::unique_ptr computeBoundedUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeBoundedUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeNextProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates); + static std::unique_ptr computeNextProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates); - static std::unique_ptr computeUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeUntilProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeGloballyProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeGloballyProbabilities(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeCumulativeRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeCumulativeRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeInstantaneousRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeInstantaneousRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeReachabilityRewards(bool minimize, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); + static std::unique_ptr computeReachabilityRewards(OptimizationDirection dir, storm::models::symbolic::NondeterministicModel const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory const& linearEquationSolverFactory); }; } diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp index b9384d9dc..f56843aef 100644 --- a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -21,12 +21,14 @@ namespace storm { } template - bool SparsePropositionalModelChecker::canHandle(storm::logic::Formula const& formula) const { + bool SparsePropositionalModelChecker::canHandle(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isPropositionalFormula(); } template - std::unique_ptr SparsePropositionalModelChecker::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) { + std::unique_ptr SparsePropositionalModelChecker::checkBooleanLiteralFormula(CheckTask const& checkTask) { + storm::logic::BooleanLiteralFormula const& stateFormula = checkTask.getFormula(); if (stateFormula.isTrueFormula()) { return std::unique_ptr(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true))); } else { @@ -35,7 +37,8 @@ namespace storm { } template - std::unique_ptr SparsePropositionalModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { + std::unique_ptr SparsePropositionalModelChecker::checkAtomicLabelFormula(CheckTask const& checkTask) { + storm::logic::AtomicLabelFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(model.hasLabel(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); return std::unique_ptr(new ExplicitQualitativeCheckResult(model.getStates(stateFormula.getLabel()))); } diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.h b/src/modelchecker/propositional/SparsePropositionalModelChecker.h index 9565a4bc9..e0bd83bff 100644 --- a/src/modelchecker/propositional/SparsePropositionalModelChecker.h +++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.h @@ -16,9 +16,9 @@ namespace storm { explicit SparsePropositionalModelChecker(SparseModelType const& model); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override; - virtual std::unique_ptr checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr checkBooleanLiteralFormula(CheckTask const& checkTask) override; + virtual std::unique_ptr checkAtomicLabelFormula(CheckTask const& checkTask) override; protected: /*! diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp index 328c0f109..943ecf7db 100644 --- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp +++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp @@ -21,12 +21,14 @@ namespace storm { } template - bool SymbolicPropositionalModelChecker::canHandle(storm::logic::Formula const& formula) const { + bool SymbolicPropositionalModelChecker::canHandle(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isPropositionalFormula(); } template - std::unique_ptr SymbolicPropositionalModelChecker::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) { + std::unique_ptr SymbolicPropositionalModelChecker::checkBooleanLiteralFormula(CheckTask const& checkTask) { + storm::logic::BooleanLiteralFormula const& stateFormula = checkTask.getFormula(); if (stateFormula.isTrueFormula()) { return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getReachableStates())); } else { @@ -35,13 +37,15 @@ namespace storm { } template - std::unique_ptr SymbolicPropositionalModelChecker::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) { + std::unique_ptr SymbolicPropositionalModelChecker::checkAtomicLabelFormula(CheckTask const& checkTask) { + storm::logic::AtomicLabelFormula const& stateFormula = checkTask.getFormula(); STORM_LOG_THROW(model.hasLabel(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'."); return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getStates(stateFormula.getLabel()))); } template - std::unique_ptr SymbolicPropositionalModelChecker::checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula) { + std::unique_ptr SymbolicPropositionalModelChecker::checkAtomicExpressionFormula(CheckTask const& checkTask) { + storm::logic::AtomicExpressionFormula const& stateFormula = checkTask.getFormula(); return std::unique_ptr(new SymbolicQualitativeCheckResult(model.getReachableStates(), model.getStates(stateFormula.getExpression()))); } diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h index 539fbff8d..d11896900 100644 --- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h +++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h @@ -21,10 +21,10 @@ namespace storm { explicit SymbolicPropositionalModelChecker(storm::models::symbolic::Model const& model); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override; - virtual std::unique_ptr checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override; - virtual std::unique_ptr checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula) override; + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr checkBooleanLiteralFormula(CheckTask const& checkTask) override; + virtual std::unique_ptr checkAtomicLabelFormula(CheckTask const& checkTask) override; + virtual std::unique_ptr checkAtomicExpressionFormula(CheckTask const& checkTask) override; protected: /*! diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index e01987f3f..bec0e7d3a 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -79,18 +79,17 @@ namespace storm { } template - SparseDtmcEliminationModelChecker::SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model, bool computeResultsForInitialStatesOnly) : SparsePropositionalModelChecker(model), computeResultsForInitialStatesOnly(computeResultsForInitialStatesOnly) { + SparseDtmcEliminationModelChecker::SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model) : SparsePropositionalModelChecker(model) { // Intentionally left empty. } template - bool SparseDtmcEliminationModelChecker::canHandle(storm::logic::Formula const& formula) const { + bool SparseDtmcEliminationModelChecker::canHandle(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); if (formula.isProbabilityOperatorFormula()) { - storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); - return this->canHandle(probabilityOperatorFormula.getSubformula()); + return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula())); } else if (formula.isRewardOperatorFormula()) { - storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula(); - return this->canHandle(rewardOperatorFormula.getSubformula()); + return this->canHandle(checkTask.replaceFormula(formula.asRewardOperatorFormula().getSubformula())); } else if (formula.isUntilFormula() || formula.isEventuallyFormula()) { if (formula.isUntilFormula()) { storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula(); @@ -134,7 +133,8 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageProbabilities(CheckTask const& checkTask) { + storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); @@ -149,7 +149,7 @@ namespace storm { storm::storage::BitVector const& initialStates = this->getModel().getInitialStates(); STORM_LOG_THROW(initialStates.getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); - STORM_LOG_THROW(this->computeResultsForInitialStatesOnly, storm::exceptions::IllegalArgumentException, "Cannot compute long-run probabilities for all states."); + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::IllegalArgumentException, "Cannot compute long-run probabilities for all states."); storm::storage::SparseMatrix backwardTransitions = this->getModel().getBackwardTransitions(); storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), psiStates); @@ -158,7 +158,7 @@ namespace storm { // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; - if (computeResultsForInitialStatesOnly && initialStates.isDisjointFrom(maybeStates)) { + if (checkTask.isOnlyInitialStatesRelevantSet() && initialStates.isDisjointFrom(maybeStates)) { STORM_LOG_DEBUG("The long-run probability for all initial states was found in a preprocessing step."); furtherComputationNeeded = false; } @@ -168,7 +168,7 @@ namespace storm { } if (furtherComputationNeeded) { - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // Determine the set of states that is reachable from the initial state without jumping over a target state. storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(transitionMatrix, initialStates, storm::storage::BitVector(numberOfStates, true), storm::storage::BitVector(numberOfStates, false)); @@ -178,12 +178,12 @@ namespace storm { std::vector stateValues(maybeStates.size(), storm::utility::zero()); storm::utility::vector::setVectorValues(stateValues, psiStates, storm::utility::one()); - result = computeLongRunValues(transitionMatrix, backwardTransitions, initialStates, maybeStates, computeResultsForInitialStatesOnly, stateValues); + result = computeLongRunValues(transitionMatrix, backwardTransitions, initialStates, maybeStates, checkTask.isOnlyInitialStatesRelevantSet(), stateValues); } // Construct check result based on whether we have computed values for all states or just the initial states. std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // If we computed the results for the initial states only, we need to filter the result to only // communicate these results. checkResult->filter(ExplicitQualitativeCheckResult(initialStates)); @@ -192,14 +192,14 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeLongRunAverageRewards(CheckTask const& checkTask) { // Do some sanity checks to establish some required properties. - RewardModelType const& rewardModel = this->getModel().getRewardModel(rewardModelName ? rewardModelName.get() : ""); + RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : ""); STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); storm::storage::BitVector const& initialStates = this->getModel().getInitialStates(); STORM_LOG_THROW(initialStates.getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); - STORM_LOG_THROW(this->computeResultsForInitialStatesOnly, storm::exceptions::IllegalArgumentException, "Cannot compute long-run probabilities for all states."); + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::IllegalArgumentException, "Cannot compute long-run probabilities for all states."); storm::storage::SparseMatrix const& transitionMatrix = this->getModel().getTransitionMatrix(); uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); @@ -225,12 +225,12 @@ namespace storm { // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; - if (computeResultsForInitialStatesOnly && initialStates.isDisjointFrom(maybeStates)) { + if (checkTask.isOnlyInitialStatesRelevantSet() && initialStates.isDisjointFrom(maybeStates)) { furtherComputationNeeded = false; } if (furtherComputationNeeded) { - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // Determine the set of states that is reachable from the initial state without jumping over a target state. storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(transitionMatrix, initialStates, storm::storage::BitVector(numberOfStates, true), storm::storage::BitVector(numberOfStates, false)); @@ -238,12 +238,12 @@ namespace storm { maybeStates &= reachableStates; } - result = computeLongRunValues(transitionMatrix, backwardTransitions, initialStates, maybeStates, computeResultsForInitialStatesOnly, stateRewardValues); + result = computeLongRunValues(transitionMatrix, backwardTransitions, initialStates, maybeStates, checkTask.isOnlyInitialStatesRelevantSet(), stateRewardValues); } // Construct check result based on whether we have computed values for all states or just the initial states. std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // If we computed the results for the initial states only, we need to filter the result to only // communicate these results. checkResult->filter(ExplicitQualitativeCheckResult(initialStates)); @@ -397,7 +397,9 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeBoundedUntilProbabilities(CheckTask const& checkTask) { + storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula(); + // Retrieve the appropriate bitvectors by model checking the subformulas. std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -411,7 +413,7 @@ namespace storm { // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; - if (computeResultsForInitialStatesOnly && this->getModel().getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) { + if (checkTask.isOnlyInitialStatesRelevantSet() && this->getModel().getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) { STORM_LOG_DEBUG("The probability for all initial states was found in a preprocessing step."); furtherComputationNeeded = false; } else if (statesWithProbabilityGreater0.empty()) { @@ -427,7 +429,7 @@ namespace storm { if (furtherComputationNeeded) { uint_fast64_t timeBound = pathFormula.getDiscreteTimeBound(); - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // Determine the set of states that is reachable from the initial state without jumping over a target state. storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(transitionMatrix, initialStates, phiStates, psiStates, true, timeBound); @@ -440,7 +442,7 @@ namespace storm { std::vector distancesFromInitialStates; storm::storage::BitVector relevantStates; - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // Determine the set of initial states of the sub-model. storm::storage::BitVector subInitialStates = this->getModel().getInitialStates() % statesWithProbabilityGreater0; @@ -469,7 +471,7 @@ namespace storm { // If we are computing the results for the initial states only, we can use the minimal distance from // each state to the initial states to determine whether we still need to consider the values for // these states. If not, we can null-out all their probabilities. - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { for (auto state : relevantStates) { if (distancesFromInitialStates[state] > (timeBound - timeStep)) { for (auto& element : submatrix.getRow(state)) { @@ -489,7 +491,7 @@ namespace storm { // Construct check result based on whether we have computed values for all states or just the initial states. std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // If we computed the results for the initial (and prob 0 and prob1) states only, we need to filter the // result to only communicate these results. checkResult->filter(ExplicitQualitativeCheckResult(this->getModel().getInitialStates() | psiStates)); @@ -498,7 +500,9 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); + // Retrieve the appropriate bitvectors by model checking the subformulas. std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -513,7 +517,7 @@ namespace storm { // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; - if (computeResultsForInitialStatesOnly && this->getModel().getInitialStates().isDisjointFrom(maybeStates)) { + if (checkTask.isOnlyInitialStatesRelevantSet() && this->getModel().getInitialStates().isDisjointFrom(maybeStates)) { STORM_LOG_DEBUG("The probability for all initial states was found in a preprocessing step."); furtherComputationNeeded = false; } else if (maybeStates.empty()) { @@ -525,7 +529,7 @@ namespace storm { if (furtherComputationNeeded) { // If we compute the results for the initial states only, we can cut off all maybe state that are not // reachable from them. - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // Determine the set of states that is reachable from the initial state without jumping over a target state. storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, statesWithProbability1); @@ -543,7 +547,7 @@ namespace storm { storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); - std::vector subresult = computeReachabilityValues(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, computeResultsForInitialStatesOnly, phiStates, psiStates, oneStepProbabilities); + std::vector subresult = computeReachabilityValues(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, checkTask.isOnlyInitialStatesRelevantSet(), phiStates, psiStates, oneStepProbabilities); storm::utility::vector::setVectorValues(result, maybeStates, subresult); } @@ -553,7 +557,7 @@ namespace storm { // Construct check result based on whether we have computed values for all states or just the initial states. std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // If we computed the results for the initial (and prob 0 and prob1) states only, we need to filter the // result to only communicate these results. checkResult->filter(ExplicitQualitativeCheckResult(~maybeStates | this->getModel().getInitialStates())); @@ -562,14 +566,16 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { + std::unique_ptr SparseDtmcEliminationModelChecker::computeReachabilityRewards(CheckTask const& checkTask) { + storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula(); + // Retrieve the appropriate bitvectors by model checking the subformulas. std::unique_ptr subResultPointer = this->check(rewardPathFormula.getSubformula()); storm::storage::BitVector phiStates(this->getModel().getNumberOfStates(), true); storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); // Do some sanity checks to establish some required properties. - RewardModelType const& rewardModel = this->getModel().getRewardModel(rewardModelName ? rewardModelName.get() : ""); + RewardModelType const& rewardModel = this->getModel().getRewardModel(checkTask.isRewardModelSet() ? checkTask.getRewardModel() : ""); STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::IllegalArgumentException, "Input model does not have a reward model."); // Then, compute the subset of states that has a reachability reward less than infinity. @@ -580,7 +586,7 @@ namespace storm { // Determine whether we need to perform some further computation. bool furtherComputationNeeded = true; - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { if (this->getModel().getInitialStates().isSubsetOf(infinityStates)) { STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); furtherComputationNeeded = false; @@ -595,7 +601,7 @@ namespace storm { if (furtherComputationNeeded) { // If we compute the results for the initial states only, we can cut off all maybe state that are not // reachable from them. - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // Determine the set of states that is reachable from the initial state without jumping over a target state. storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, psiStates); @@ -613,7 +619,7 @@ namespace storm { // Project the state reward vector to all maybe-states. std::vector stateRewardValues = rewardModel.getTotalRewardVector(maybeStates.getNumberOfSetBits(), this->getModel().getTransitionMatrix(), maybeStates); - std::vector subresult = computeReachabilityValues(submatrix, stateRewardValues, submatrixTransposed, newInitialStates, computeResultsForInitialStatesOnly, phiStates, psiStates, this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates)); + std::vector subresult = computeReachabilityValues(submatrix, stateRewardValues, submatrixTransposed, newInitialStates, checkTask.isOnlyInitialStatesRelevantSet(), phiStates, psiStates, this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates)); storm::utility::vector::setVectorValues(result, maybeStates, subresult); } @@ -623,7 +629,7 @@ namespace storm { // Construct check result based on whether we have computed values for all states or just the initial states. std::unique_ptr checkResult(new ExplicitQuantitativeCheckResult(result)); - if (computeResultsForInitialStatesOnly) { + if (checkTask.isOnlyInitialStatesRelevantSet()) { // If we computed the results for the initial (and inf) states only, we need to filter the result to // only communicate these results. checkResult->filter(ExplicitQualitativeCheckResult(~maybeStates | this->getModel().getInitialStates())); @@ -632,8 +638,8 @@ namespace storm { } template - std::unique_ptr SparseDtmcEliminationModelChecker::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); + std::unique_ptr SparseDtmcEliminationModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { + storm::logic::ConditionalPathFormula const& pathFormula = checkTask.getFormula(); // Retrieve the appropriate bitvectors by model checking the subformulas. STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula."); @@ -648,7 +654,7 @@ namespace storm { // Do some sanity checks to establish some required properties. // STORM_LOG_WARN_COND(storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, "The chosen elimination method is not available for computing conditional probabilities. Falling back to regular state elimination."); STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); - STORM_LOG_THROW(this->computeResultsForInitialStatesOnly, storm::exceptions::IllegalArgumentException, "Cannot compute conditional probabilities for all states."); + STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::IllegalArgumentException, "Cannot compute conditional probabilities for all states."); storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); storm::storage::SparseMatrix backwardTransitions = this->getModel().getBackwardTransitions(); @@ -677,18 +683,10 @@ namespace storm { storm::storage::BitVector statesReachingPhi = storm::utility::graph::performProbGreater0(backwardTransitions, trueStates, phiStates); // The set of states we need to consider are those that have a non-zero probability to satisfy the condition or are on some path that has a psi state in it. - STORM_LOG_TRACE("Initial state: " << this->getModel().getInitialStates()); - STORM_LOG_TRACE("Phi states: " << phiStates); - STORM_LOG_TRACE("Psi state: " << psiStates); - STORM_LOG_TRACE("States with probability greater 0 of satisfying the condition: " << statesWithProbabilityGreater0); - STORM_LOG_TRACE("States with psi predecessor: " << statesWithPsiPredecessor); - STORM_LOG_TRACE("States reaching phi: " << statesReachingPhi); storm::storage::BitVector maybeStates = statesWithProbabilityGreater0 | (statesWithPsiPredecessor & statesReachingPhi); - STORM_LOG_TRACE("Found " << maybeStates.getNumberOfSetBits() << " relevant states: " << maybeStates); // Determine the set of initial states of the sub-DTMC. storm::storage::BitVector newInitialStates = this->getModel().getInitialStates() % maybeStates; - STORM_LOG_TRACE("Found new initial states: " << newInitialStates << " (old: " << this->getModel().getInitialStates() << ")"); // Create a dummy vector for the one-step probabilities. std::vector oneStepProbabilities(maybeStates.getNumberOfSetBits(), storm::utility::zero()); @@ -710,10 +708,7 @@ namespace storm { // Keep only the states that we do not eliminate in the maybe states. maybeStates = phiStates | psiStates; - STORM_LOG_TRACE("Phi states in reduced model " << phiStates); - STORM_LOG_TRACE("Psi states in reduced model " << psiStates); storm::storage::BitVector statesToEliminate = ~maybeStates & ~newInitialStates; - STORM_LOG_TRACE("Eliminating the states " << statesToEliminate); // Before starting the model checking process, we assign priorities to states so we can use them to // impose ordering constraints later. @@ -737,7 +732,6 @@ namespace storm { uint_fast64_t numberOfStatesToEliminate = statePriorities->size(); STORM_LOG_INFO("Eliminating " << numberOfStatesToEliminate << " states using the state elimination technique." << std::endl); performPrioritizedStateElimination(statePriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, this->getModel().getInitialStates(), true); - STORM_LOG_INFO("Eliminated " << numberOfStatesToEliminate << " states." << std::endl); storm::solver::stateelimination::ConditionalEliminator stateEliminator = storm::solver::stateelimination::ConditionalEliminator(flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, phiStates, psiStates); @@ -853,25 +847,6 @@ namespace storm { numerator += trans1.getValue() * additiveTerm; } } - std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now(); - std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now(); - - if (storm::settings::generalSettings().isShowStatisticsSet()) { - std::chrono::high_resolution_clock::duration conversionTime = conversionEnd - conversionStart; - std::chrono::milliseconds conversionTimeInMilliseconds = std::chrono::duration_cast(conversionTime); - std::chrono::high_resolution_clock::duration modelCheckingTime = modelCheckingEnd - modelCheckingStart; - std::chrono::milliseconds modelCheckingTimeInMilliseconds = std::chrono::duration_cast(modelCheckingTime); - std::chrono::high_resolution_clock::duration totalTime = totalTimeEnd - totalTimeStart; - std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast(totalTime); - - STORM_PRINT_AND_LOG(std::endl); - STORM_PRINT_AND_LOG("Time breakdown:" << std::endl); - STORM_PRINT_AND_LOG(" * time for conversion: " << conversionTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG(" * time for checking: " << modelCheckingTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG("------------------------------------------" << std::endl); - STORM_PRINT_AND_LOG(" * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG(std::endl); - } return std::unique_ptr(new ExplicitQuantitativeCheckResult(initialState, numerator / denominator)); } @@ -972,9 +947,6 @@ namespace storm { template std::vector::ValueType> SparseDtmcEliminationModelChecker::computeReachabilityValues(storm::storage::SparseMatrix const& transitionMatrix, std::vector& values, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& oneStepProbabilitiesToTarget) { - std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); - - std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. storm::storage::FlexibleSparseMatrix flexibleMatrix(transitionMatrix); storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(backwardTransitions); @@ -1002,31 +974,6 @@ namespace storm { STORM_LOG_ASSERT(flexibleMatrix.empty(), "Not all transitions were eliminated."); STORM_LOG_ASSERT(flexibleBackwardTransitions.empty(), "Not all transitions were eliminated."); - std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now(); - std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now(); - - if (storm::settings::generalSettings().isShowStatisticsSet()) { - std::chrono::high_resolution_clock::duration conversionTime = conversionEnd - conversionStart; - std::chrono::milliseconds conversionTimeInMilliseconds = std::chrono::duration_cast(conversionTime); - std::chrono::high_resolution_clock::duration modelCheckingTime = modelCheckingEnd - modelCheckingStart; - std::chrono::milliseconds modelCheckingTimeInMilliseconds = std::chrono::duration_cast(modelCheckingTime); - std::chrono::high_resolution_clock::duration totalTime = totalTimeEnd - totalTimeStart; - std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast(totalTime); - - STORM_PRINT_AND_LOG(std::endl); - STORM_PRINT_AND_LOG("Time breakdown:" << std::endl); - STORM_PRINT_AND_LOG(" * time for conversion: " << conversionTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG(" * time for checking: " << modelCheckingTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG("------------------------------------------" << std::endl); - STORM_PRINT_AND_LOG(" * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG(std::endl); - STORM_PRINT_AND_LOG("Other:" << std::endl); - STORM_PRINT_AND_LOG(" * number of states eliminated: " << transitionMatrix.getRowCount() << std::endl); - if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) { - STORM_PRINT_AND_LOG(" * maximal depth of SCC decomposition: " << maximalDepth << std::endl); - } - } - // Now, we return the value for the only initial state. STORM_LOG_DEBUG("Simplifying and returning result."); for (auto& value : values) { @@ -1290,9 +1237,6 @@ namespace storm { } if (!foundCorrespondingElement) { -// std::cout << "forward entry: " << forwardIndex << " -> " << forwardEntry << std::endl; -// transitionMatrix.print(); -// backwardTransitions.print(); return false; } } diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index bfcfbcd31..3a77c43fb 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -34,19 +34,18 @@ namespace storm { * Creates an elimination-based model checker for the given model. * * @param model The model to analyze. - * @param computeResultsForInitialStatesOnly If set to true, the results are only computed for */ - explicit SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model, bool computeResultsForInitialStatesOnly = true); + explicit SparseDtmcEliminationModelChecker(storm::models::sparse::Dtmc const& model); // The implemented methods of the AbstractModelChecker interface. - virtual bool canHandle(storm::logic::Formula const& formula) const override; - virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::LongRunAverageRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName = boost::optional(), bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageRewards(CheckTask const& checkTask) override; + virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + private: class StaticStatePriorityQueue : public StatePriorityQueue { @@ -113,9 +112,6 @@ namespace storm { static bool checkConsistent(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions); - // A flag that indicates whether this model checker is supposed to produce results for all states or just for the initial states. - bool computeResultsForInitialStatesOnly; - }; } // namespace modelchecker diff --git a/src/parser/SpiritErrorHandler.h b/src/parser/SpiritErrorHandler.h index cd2a35b06..949ad9b12 100644 --- a/src/parser/SpiritErrorHandler.h +++ b/src/parser/SpiritErrorHandler.h @@ -16,7 +16,7 @@ namespace storm { qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const { auto lineStart = boost::spirit::get_line_start(b, where); auto lineEnd = std::find(where, e, '\n'); - std::string line(++lineStart, lineEnd); + std::string line(lineStart, lineEnd); std::stringstream stream; stream << "Parsing error at " << get_line(where) << ":" << boost::spirit::get_column(lineStart, where) << ": " << " expecting " << what << ", here:" << std::endl; diff --git a/src/utility/storm.h b/src/utility/storm.h index 7ffba8c85..d4a042bc6 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -76,7 +76,7 @@ namespace storm { template - std::shared_ptr> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile = boost::optional(), boost::optional const& transitionRewardsFile = boost::optional(), boost::optional const& choiceLabelingFile = boost::optional()) { + std::shared_ptr> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile = boost::none, boost::optional const& transitionRewardsFile = boost::none, boost::optional const& choiceLabelingFile = boost::none) { return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); } @@ -236,23 +236,23 @@ namespace storm { #endif template - std::unique_ptr verifyModel(std::shared_ptr model, std::shared_ptr const& formula) { + std::unique_ptr verifyModel(std::shared_ptr model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); switch(settings.getEngine()) { case storm::settings::modules::GeneralSettings::Engine::Sparse: { std::shared_ptr> sparseModel = model->template as>(); STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model"); - return verifySparseModel(sparseModel, formula); + return verifySparseModel(sparseModel, formula, onlyInitialStatesRelevant); } case storm::settings::modules::GeneralSettings::Engine::Hybrid: { std::shared_ptr> ddModel = model->template as>(); STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Hybrid engine requires a dd input model"); - return verifySymbolicModelWithHybridEngine(ddModel, formula); + return verifySymbolicModelWithHybridEngine(ddModel, formula, onlyInitialStatesRelevant); } case storm::settings::modules::GeneralSettings::Engine::Dd: { std::shared_ptr> ddModel = model->template as>(); STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a dd input model"); - return verifySymbolicModelWithDdEngine(ddModel, formula); + return verifySymbolicModelWithDdEngine(ddModel, formula, onlyInitialStatesRelevant); } case storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement: { STORM_LOG_ASSERT(false, "This position should not be reached, as at this point no model has been built."); @@ -261,18 +261,19 @@ namespace storm { } template - std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula) { + std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { std::unique_ptr result; + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr> dtmc = model->template as>(); storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); } else { storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker2(*dtmc); - if (modelchecker2.canHandle(*formula)) { - result = modelchecker2.check(*formula); + if (modelchecker2.canHandle(task)) { + result = modelchecker2.check(task); } } } else if (model->getType() == storm::models::ModelType::Mdp) { @@ -280,20 +281,20 @@ namespace storm { #ifdef STORM_HAVE_CUDA if (settings.isCudaSet()) { storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker modelchecker(*mdp); - result = modelchecker.check(*formula); + result = modelchecker.check(task); } else { storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); - result = modelchecker.check(*formula); + result = modelchecker.check(task); } #else storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); - result = modelchecker.check(*formula); + result = modelchecker.check(task); #endif } else if (model->getType() == storm::models::ModelType::Ctmc) { std::shared_ptr> ctmc = model->template as>(); storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc); - result = modelchecker.check(*formula); + result = modelchecker.check(task); } return result; @@ -317,13 +318,14 @@ namespace storm { } template<> - inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula) { + inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { std::unique_ptr result; std::shared_ptr> dtmc = model->template as>(); storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property."); } @@ -333,25 +335,26 @@ namespace storm { #endif template - std::unique_ptr verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::shared_ptr const& formula) { + std::unique_ptr verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { std::unique_ptr result; + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr> dtmc = model->template as>(); storm::modelchecker::HybridDtmcPrctlModelChecker modelchecker(*dtmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); } } else if (model->getType() == storm::models::ModelType::Ctmc) { std::shared_ptr> ctmc = model->template as>(); storm::modelchecker::HybridCtmcCslModelChecker modelchecker(*ctmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); } } else if (model->getType() == storm::models::ModelType::Mdp) { std::shared_ptr> mdp = model->template as>(); storm::modelchecker::HybridMdpPrctlModelChecker modelchecker(*mdp); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); } } else { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); @@ -361,19 +364,20 @@ namespace storm { template - std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula) { + std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { std::unique_ptr result; + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); if (model->getType() == storm::models::ModelType::Dtmc) { std::shared_ptr> dtmc = model->template as>(); storm::modelchecker::SymbolicDtmcPrctlModelChecker modelchecker(*dtmc); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); } } else if (model->getType() == storm::models::ModelType::Mdp) { std::shared_ptr> mdp = model->template as>(); storm::modelchecker::SymbolicMdpPrctlModelChecker modelchecker(*mdp); - if (modelchecker.canHandle(*formula)) { - result = modelchecker.check(*formula); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); } } else { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); diff --git a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp index 7ce394070..ad4d9ab3d 100644 --- a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp @@ -94,14 +94,14 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\" || F \"observeIGreater1\"]"); - result = checker.check(*formula); + result = checker.check(storm::modelchecker::CheckTask(*formula).setOnlyInitialStatesRelevant(true)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.15330064292476167, quantitativeResult4[0], storm::settings::generalSettings().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\" || F \"observe0Greater1\"]"); - result = checker.check(*formula); + result = checker.check(storm::modelchecker::CheckTask(*formula).setOnlyInitialStatesRelevant(true)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.96592521978041668, quantitativeResult5[0], storm::settings::generalSettings().getPrecision()); diff --git a/test/performance/builder/leader5.nm b/test/performance/builder/leader5.nm index c48a255bb..26316affa 100644 --- a/test/performance/builder/leader5.nm +++ b/test/performance/builder/leader5.nm @@ -1,4 +1,3 @@ -<<<<<<< HEAD // asynchronous leader election // 4 processes // gxn/dxp 29/01/01 @@ -96,104 +95,3 @@ endrewards //---------------------------------------------------------------------------------------------------------------------------- formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0); label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4; - -======= -// asynchronous leader election -// 4 processes -// gxn/dxp 29/01/01 - -mdp - -const int N= 5; // number of processes - -//---------------------------------------------------------------------------------------------------------------------------- -module process1 - - // COUNTER - c1 : [0..5-1]; - - // STATES - s1 : [0..4]; - // 0 make choice - // 1 have not received neighbours choice - // 2 active - // 3 inactive - // 4 leader - - // PREFERENCE - p1 : [0..1]; - - // VARIABLES FOR SENDING AND RECEIVING - receive1 : [0..2]; - // not received anything - // received choice - // received counter - sent1 : [0..2]; - // not send anything - // sent choice - // sent counter - - // pick value - [] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1); - - // send preference - [p12] (s1=1) & (sent1=0) -> (sent1'=1); - // receive preference - // stay active - [p51] (s1=1) & (receive1=0) & !( (p1=0) & (p5=1) ) -> (s1'=2) & (receive1'=1); - // become inactive - [p51] (s1=1) & (receive1=0) & (p1=0) & (p5=1) -> (s1'=3) & (receive1'=1); - - // send preference (can now reset preference) - [p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0); - // send counter (already sent preference) - // not received counter yet - [c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2); - // received counter (pick again) - [c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); - - // receive counter and not sent yet (note in this case do not pass it on as will send own counter) - [c51] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2); - // receive counter and sent counter - // only active process (decide) - [c51] (s1=2) & (receive1=1) & (sent1=2) & (c5=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); - // other active process (pick again) - [c51] (s1=2) & (receive1=1) & (sent1=2) & (c5 (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); - - // send preference (must have received preference) and can now reset - [p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0); - // send counter (must have received counter first) and can now reset - [c12] (s1=3) & (receive1=2) & (sent1=1) -> (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); - - // receive preference - [p51] (s1=3) & (receive1=0) -> (p1'=p5) & (receive1'=1); - // receive counter - [c51] (s1=3) & (receive1=1) & (c5 (c1'=c5+1) & (receive1'=2); - - // done - [done] (s1=4) -> (s1'=s1); - // add loop for processes who are inactive - [done] (s1=3) -> (s1'=s1); - -endmodule - -//---------------------------------------------------------------------------------------------------------------------------- - -// construct further stations through renaming -module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p51=p12,c12=c23,c51=c12,p5=p1,c5=c1] endmodule -module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p51=p23,c12=c34,c51=c23,p5=p2,c5=c2] endmodule -module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p51=p34,c12=c45,c51=c34,p5=p3,c5=c3] endmodule -module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p51,p51=p45,c12=c51,c51=c45,p5=p4,c5=c4] endmodule - -//---------------------------------------------------------------------------------------------------------------------------- - -// reward - expected number of rounds (equals the number of times a process receives a counter) -rewards "rounds" - [c12] true : 1; -endrewards - -//---------------------------------------------------------------------------------------------------------------------------- -formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0); -label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4; - ->>>>>>> 90d2b218a044edca8062084ee89d171695149c1e diff --git a/test/performance/builder/leader5_8.pm b/test/performance/builder/leader5_8.pm index e6cfc2106..eb7dd9fd7 100644 --- a/test/performance/builder/leader5_8.pm +++ b/test/performance/builder/leader5_8.pm @@ -1,4 +1,3 @@ -<<<<<<< HEAD // synchronous leader election protocol (itai & Rodeh) // dxp/gxn 25/01/01 @@ -88,96 +87,3 @@ endrewards // labels label "elected" = s1=3&s2=3&s3=3&s4=3&s5=3; - -======= -// synchronous leader election protocol (itai & Rodeh) -// dxp/gxn 25/01/01 - -dtmc - -// CONSTANTS -const int N = 5; // number of processes -const int K = 8; // range of probabilistic choice - -// counter module used to count the number of processes that have been read -// and to know when a process has decided -module counter - - // counter (c=i means process j reading process (i-1)+j next) - c : [1..N-1]; - - // reading - [read] c (c'=c+1); - // finished reading - [read] c=N-1 -> (c'=c); - //decide - [done] u1|u2|u3|u4|u5 -> (c'=c); - // pick again reset counter - [retry] !(u1|u2|u3|u4|u5) -> (c'=1); - // loop (when finished to avoid deadlocks) - [loop] s1=3 -> (c'=c); - -endmodule - -// processes form a ring and suppose: -// process 1 reads process 2 -// process 2 reads process 3 -// process 3 reads process 1 -module process1 - - // local state - s1 : [0..3]; - // s1=0 make random choice - // s1=1 reading - // s1=2 deciding - // s1=3 finished - - // has a unique id so far (initially true) - u1 : bool; - - // value to be sent to next process in the ring (initially sets this to its own value) - v1 : [0..K-1]; - - // random choice - p1 : [0..K-1]; - - // pick value - [pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true) - + 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true) - + 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true) - + 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true) - + 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true) - + 1/K : (s1'=1) & (p1'=5) & (v1'=5) & (u1'=true) - + 1/K : (s1'=1) & (p1'=6) & (v1'=6) & (u1'=true) - + 1/K : (s1'=1) & (p1'=7) & (v1'=7) & (u1'=true); - // read - [read] s1=1 & u1 & c (u1'=(p1!=v2)) & (v1'=v2); - [read] s1=1 & !u1 & c (u1'=false) & (v1'=v2) & (p1'=0); - // read and move to decide - [read] s1=1 & u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); - [read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0); - // deciding - // done - [done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); - //retry - [retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); - // loop (when finished to avoid deadlocks) - [loop] s1=3 -> (s1'=3); - -endmodule - -// construct remaining processes through renaming -module process2 = process1 [ s1=s2,p1=p2,v1=v2,u1=u2,v2=v3 ] endmodule -module process3 = process1 [ s1=s3,p1=p3,v1=v3,u1=u3,v2=v4 ] endmodule -module process4 = process1 [ s1=s4,p1=p4,v1=v4,u1=u4,v2=v5 ] endmodule -module process5 = process1 [ s1=s5,p1=p5,v1=v5,u1=u5,v2=v1 ] endmodule - -// expected number of rounds -rewards "num_rounds" - [pick] true : 1; -endrewards - -// labels -label "elected" = s1=3&s2=3&s3=3&s4=3&s5=3; - ->>>>>>> 90d2b218a044edca8062084ee89d171695149c1e