From fc24c5596074807d1587108196f193742ebd84f6 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 26 May 2016 21:40:04 +0200 Subject: [PATCH] some preprocessing for multi-objective formulas Former-commit-id: 3a909154f77c6b7f699833bc8b3752674b67d9b6 --- src/CMakeLists.txt | 5 +- src/logic/FragmentChecker.cpp | 3 + src/logic/FragmentSpecification.cpp | 18 +- src/logic/FragmentSpecification.h | 4 + src/logic/MultiObjectiveFormula.cpp | 25 +- src/logic/MultiObjectiveFormula.h | 10 +- src/modelchecker/AbstractModelChecker.cpp | 7 + src/modelchecker/AbstractModelChecker.h | 6 +- .../SparseMdpMultiObjectiveModelChecker.cpp | 46 ++++ .../SparseMdpMultiObjectiveModelChecker.h | 27 ++ ...seMdpMultiObjectivePreprocessingHelper.cpp | 254 ++++++++++++++++++ ...arseMdpMultiObjectivePreprocessingHelper.h | 62 +++++ ...rseMultiObjectiveModelCheckerInformation.h | 83 ++++++ src/utility/storm.h | 17 +- test/functional/logic/FragmentCheckerTest.cpp | 40 +++ 15 files changed, 590 insertions(+), 17 deletions(-) create mode 100644 src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp create mode 100644 src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h create mode 100644 src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp create mode 100644 src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h create mode 100644 src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 34b3cf77b..35d2e1d92 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -24,6 +24,8 @@ file(GLOB_RECURSE STORM_MODELCHECKER_CSL_HELPER_FILES ${PROJECT_SOURCE_DIR}/src/ file(GLOB_RECURSE STORM_MODELCHECKER_REACHABILITY_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_EXPLORATION_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/exploration/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/exploration/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_PROPOSITIONAL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.cpp) +file(GLOB STORM_MODELCHECKER_MULTIOBJECTIVE_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/multiobjective/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/multiobjective/*.cpp) +file(GLOB_RECURSE STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/multiobjective/helper/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/multiobjective/helper/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_RESULTS_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.cpp) file(GLOB_RECURSE STORM_COUNTEREXAMPLES_FILES ${PROJECT_SOURCE_DIR}/src/counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/counterexamples/*.cpp) file(GLOB_RECURSE STORM_PERMISSIVESCHEDULER_FILES ${PROJECT_SOURCE_DIR}/src/permissivesched/*.h ${PROJECT_SOURCE_DIR}/src/permissivesched/*.cpp) @@ -78,6 +80,8 @@ source_group(modelchecker\\csl\\helper FILES ${STORM_MODELCHECKER_CSL_HELPER_FIL source_group(modelchecker\\exploration FILES ${STORM_MODELCHECKER_EXPLORATION_FILES}) source_group(modelchecker\\reachability FILES ${STORM_MODELCHECKER_REACHABILITY_FILES}) source_group(modelchecker\\propositional FILES ${STORM_MODELCHECKER_PROPOSITIONAL_FILES}) +source_group(modelchecker\\multiobjective FILES ${STORM_MODELCHECKER_MULTIOBJECTIVE_FILES}) +source_group(modelchecker\\multiobjective\\helper FILES ${STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_FILES}) source_group(modelchecker\\results FILES ${STORM_MODELCHECKER_RESULTS_FILES}) source_group(counterexamples FILES ${STORM_COUNTEREXAMPLES_FILES}) source_group(permissiveschedulers FILES ${STORM_PERMISSIVESCHEDULER_FILES}) @@ -133,7 +137,6 @@ set_target_properties(storm-dft-main PROPERTIES OUTPUT_NAME "storm-dft") target_link_libraries(storm ${STORM_LINK_LIBRARIES}) - INSTALL(TARGETS storm-main RUNTIME DESTINATION bin LIBRARY DESTINATION lib diff --git a/src/logic/FragmentChecker.cpp b/src/logic/FragmentChecker.cpp index 26a787455..b4bda1f8f 100644 --- a/src/logic/FragmentChecker.cpp +++ b/src/logic/FragmentChecker.cpp @@ -166,6 +166,9 @@ namespace storm { if(!inherited.getSpecification().areNestedMultiObjectiveFormulasAllowed()){ subFormulaFragment.setMultiObjectiveFormulasAllowed(false); } + if(!inherited.getSpecification().areNestedOperatorsInsideMultiObjectiveFormulasAllowed()){ + subFormulaFragment.setNestedOperatorsAllowed(false); + } bool result = inherited.getSpecification().areMultiObjectiveFormulasAllowed(); for(uint_fast64_t index = 0; indexnestedMultiObjectiveFormulas = newValue; return *this; } - + + bool FragmentSpecification::areNestedOperatorsInsideMultiObjectiveFormulasAllowed() const { + return this->nestedOperatorsInsideMultiObjectiveFormulas; + } + + FragmentSpecification& FragmentSpecification::setNestedOperatorsInsideMultiObjectiveFormulasAllowed(bool newValue) { + this->nestedOperatorsInsideMultiObjectiveFormulas = newValue; + return *this; + } + bool FragmentSpecification::areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const { return this->onlyEventuallyFormuluasInConditionalFormulas; } diff --git a/src/logic/FragmentSpecification.h b/src/logic/FragmentSpecification.h index c53b287d0..88910988d 100644 --- a/src/logic/FragmentSpecification.h +++ b/src/logic/FragmentSpecification.h @@ -88,6 +88,9 @@ namespace storm { bool areNestedMultiObjectiveFormulasAllowed() const; FragmentSpecification& setNestedMultiObjectiveFormulasAllowed(bool newValue); + bool areNestedOperatorsInsideMultiObjectiveFormulasAllowed() const; + FragmentSpecification& setNestedOperatorsInsideMultiObjectiveFormulasAllowed(bool newValue); + bool areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const; FragmentSpecification& setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue); @@ -148,6 +151,7 @@ namespace storm { bool nestedOperators; bool nestedPathFormulas; bool nestedMultiObjectiveFormulas; + bool nestedOperatorsInsideMultiObjectiveFormulas; bool onlyEventuallyFormuluasInConditionalFormulas; bool stepBoundedUntilFormulas; bool timeBoundedUntilFormulas; diff --git a/src/logic/MultiObjectiveFormula.cpp b/src/logic/MultiObjectiveFormula.cpp index 22d02b40d..4717fd1e4 100644 --- a/src/logic/MultiObjectiveFormula.cpp +++ b/src/logic/MultiObjectiveFormula.cpp @@ -30,7 +30,24 @@ namespace storm { bool MultiObjectiveFormula::hasQuantitativeResult() const { return !hasQualitativeResult(); - }; + } + + bool MultiObjectiveFormula::hasNumericalResult() const { + bool hasExactlyOneQualitativeSubformula = false; + for(auto const& subformula : this->subformulas){ + if(subformula->hasQualitativeResult()){ + if(hasExactlyOneQualitativeSubformula){ + return false; + } + hasExactlyOneQualitativeSubformula=true; + } + } + return hasExactlyOneQualitativeSubformula; + } + + bool MultiObjectiveFormula::hasParetoCurveResult() const { + return hasQuantitativeResult() && !hasNumericalResult(); + } Formula const& MultiObjectiveFormula::getSubformula(uint_fast64_t index) const { STORM_LOG_THROW(index < getNumberOfSubformulas(), storm::exceptions::InvalidArgumentException, "Tried to access subformula with index " << index << " but there are only " << this->getNumberOfSubformulas() << " subformulas."); @@ -41,6 +58,10 @@ namespace storm { return this->subformulas.size(); } + std::vector> const& MultiObjectiveFormula::getSubFormulas() const { + return this->subformulas; + } + boost::any MultiObjectiveFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } @@ -75,4 +96,4 @@ namespace storm { return out; } } -} \ No newline at end of file +} diff --git a/src/logic/MultiObjectiveFormula.h b/src/logic/MultiObjectiveFormula.h index 7647300ac..0e597d89f 100644 --- a/src/logic/MultiObjectiveFormula.h +++ b/src/logic/MultiObjectiveFormula.h @@ -13,12 +13,14 @@ namespace storm { virtual bool isMultiObjectiveFormula() const override; - virtual bool hasQualitativeResult() const override; - virtual bool hasQuantitativeResult() const override; + virtual bool hasQualitativeResult() const override; // Result is true or false + virtual bool hasQuantitativeResult() const override; // Result is numerical or a pareto curve + virtual bool hasNumericalResult() const; // Result is numerical + virtual bool hasParetoCurveResult() const; // Result is a pareto curve Formula const& getSubformula(uint_fast64_t index) const; uint_fast64_t getNumberOfSubformulas() const; - + std::vector> const& getSubFormulas() const; virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; @@ -32,4 +34,4 @@ namespace storm { } } -#endif /* STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_ */ \ No newline at end of file +#endif /* STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_ */ diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 4fd86a13e..2e9ac6e43 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -14,6 +14,9 @@ namespace storm { std::unique_ptr AbstractModelChecker::check(CheckTask const& checkTask) { storm::logic::Formula const& formula = checkTask.getFormula(); STORM_LOG_THROW(this->canHandle(checkTask), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'."); + if (formula.isMultiObjectiveFormula()){ + return this->checkMultiObjectiveFormula(checkTask.substituteFormula(formula.asMultiObjectiveFormula())); + } if (formula.isStateFormula()) { return this->checkStateFormula(checkTask.substituteFormula(formula.asStateFormula())); } @@ -240,5 +243,9 @@ namespace storm { } return subResult; } + + std::unique_ptr AbstractModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); + } } } diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index b6f009197..da69db224 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -69,8 +69,12 @@ namespace storm { virtual std::unique_ptr checkTimeOperatorFormula(CheckTask const& checkTask); virtual std::unique_ptr checkLongRunAverageOperatorFormula(CheckTask const& checkTask); virtual std::unique_ptr checkUnaryBooleanStateFormula(CheckTask const& checkTask); + + // The methods to check multi-objective formulas. + virtual std::unique_ptr checkMultiObjectiveFormula(CheckTask const& checkTask); + }; } } -#endif /* STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ */ \ No newline at end of file +#endif /* STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ */ diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp new file mode 100644 index 000000000..7d94481f8 --- /dev/null +++ b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp @@ -0,0 +1,46 @@ +#include "src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h" + +#include "src/utility/macros.h" +#include "src/logic/Formulas.h" +#include "src/logic/FragmentSpecification.h" + +#include "src/models/sparse/StandardRewardModel.h" + +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" + +#include "src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h" +#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h" + +#include "src/exceptions/NotImplementedException.h" + +namespace storm { + namespace modelchecker { + template + SparseMdpMultiObjectiveModelChecker::SparseMdpMultiObjectiveModelChecker(SparseMdpModelType const& model) : SparseMdpPrctlModelChecker(model) { + // Intentionally left empty. + } + + template + bool SparseMdpMultiObjectiveModelChecker::canHandle(CheckTask const& checkTask) const { + // A formula without multi objective (sub)formulas can be handled by the base class + if(SparseMdpPrctlModelChecker::canHandle(checkTask)) return true; + //In general, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude this. + if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; + if(!checkTask.isOnlyInitialStatesRelevantSet()) return false; + return checkTask.getFormula().isInFragment(storm::logic::multiObjective()); + } + + template + std::unique_ptr SparseMdpMultiObjectiveModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { + + helper::SparseMultiObjectiveModelCheckerInformation info = helper::SparseMdpMultiObjectivePreprocessingHelper::preprocess(checkTask.getFormula(), this->getModel()); + + return std::unique_ptr(new ExplicitQualitativeCheckResult()); + } + + + + template class SparseMdpMultiObjectiveModelChecker>; + } +} diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h new file mode 100644 index 000000000..f6e1efdf9 --- /dev/null +++ b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h @@ -0,0 +1,27 @@ +#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMDPMULTIOBJECTIVEMODELCHECKER_H_ +#define STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMDPMULTIOBJECTIVEMODELCHECKER_H_ + +#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" + +namespace storm { + namespace modelchecker { + template + class SparseMdpMultiObjectiveModelChecker : public SparseMdpPrctlModelChecker { + public: + typedef typename SparseMdpModelType::ValueType ValueType; + typedef typename SparseMdpModelType::RewardModelType RewardModelType; + + explicit SparseMdpMultiObjectiveModelChecker(SparseMdpModelType const& model); + + virtual bool canHandle(CheckTask const& checkTask) const override; + + virtual std::unique_ptr checkMultiObjectiveFormula(CheckTask const& checkTask) override; + + private: + + + }; + } // namespace modelchecker +} // namespace storm + +#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_SPARSEMDPMULTIOBJECTIVEMODELCHECKER_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp new file mode 100644 index 000000000..4366fc1a8 --- /dev/null +++ b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.cpp @@ -0,0 +1,254 @@ + #include "src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h" + +#include "src/models/sparse/Mdp.h" +#include "src/models/sparse/StandardRewardModel.h" + +#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" + +#include "src/storage/BitVector.h" + +#include "src/utility/macros.h" +#include "src/utility/vector.h" +#include "src/utility/graph.h" + +#include "src/exceptions/InvalidPropertyException.h" +#include "src/exceptions/UnexpectedException.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + template + SparseMultiObjectiveModelCheckerInformation SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseMdpModelType originalModel) { + Information info(std::move(originalModel)); + + //Initialize the state mapping. + info.getNewToOldStateMapping().reserve(info.getModel().getNumberOfStates()); + for(uint_fast64_t state = 0; state < info.getModel().getNumberOfStates(); ++state){ + info.getNewToOldStateMapping().push_back(state); + } + + //Gather information regarding the individual objectives + if(!gatherObjectiveInformation(originalFormula, info)){ + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not gather information for objectives " << originalFormula << "."); + } + + // Find out whether negative rewards should be considered. + if(!setWhetherNegativeRewardsAreConsidered(info)){ + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not find out whether to consider negative rewards " << originalFormula << "."); + } + + //Invoke preprocessing on objectives + bool success = false; + for (auto& obj : info.getObjectives()){ + STORM_LOG_DEBUG("Preprocessing objective " << *obj.originalFormula << "."); + if(obj.originalFormula->isProbabilityOperatorFormula()){ + success = preprocess(obj.originalFormula->asProbabilityOperatorFormula(), info, obj); + } else if(obj.originalFormula->isRewardOperatorFormula()){ + success = preprocess(obj.originalFormula->asRewardOperatorFormula(), info, obj); + } + } + STORM_LOG_THROW(success, storm::exceptions::InvalidPropertyException, "Could not preprocess for the formula " << originalFormula << "."); + return info; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::gatherObjectiveInformation(storm::logic::MultiObjectiveFormula const& formula, Information& info) { + for(auto const& subF : formula.getSubFormulas()){ + if(!subF->isOperatorFormula()){ + STORM_LOG_ERROR("Expected an OperatorFormula as subformula of " << formula << " but got " << *subF); + return false; + } + storm::logic::OperatorFormula const& f = subF->asOperatorFormula(); + typename Information::ObjectiveInformation objective; + + objective.originalFormula = subF; + + if(f.hasBound()){ + objective.threshold = f.getBound().threshold; + // Note that we minimize if the comparison type is an upper bound since we are interested in the EXISTENCE of a scheduler... + objective.originalFormulaMinimizes = !storm::logic::isLowerBound(f.getBound().comparisonType); + } else if (f.hasOptimalityType()){ + objective.originalFormulaMinimizes = storm::solver::minimize(f.getOptimalityType()); + } else { + STORM_LOG_ERROR("Current objective" << f << "does not specify whether to minimize or maximize"); + } + + objective.rewardModelName = "objective" + std::to_string(info.getObjectives().size()); + // Make sure the new reward model gets a unique name + while(info.getModel().hasRewardModel(objective.rewardModelName)){ + objective.rewardModelName = "_" + objective.rewardModelName; + } + + if(!setStepBoundOfObjective(objective)) { + return false; + } + + info.getObjectives().push_back(std::move(objective)); + } + return true; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::setStepBoundOfObjective(typename Information::ObjectiveInformation& objective){ + if(objective.originalFormula->isProbabilityOperatorFormula()){ + storm::logic::Formula const& f = objective.originalFormula->asProbabilityOperatorFormula().getSubformula(); + if(f.isBoundedUntilFormula()){ + if(f.asBoundedUntilFormula().hasDiscreteTimeBound()){ + objective.stepBound = f.asBoundedUntilFormula().getDiscreteTimeBound(); + } else { + STORM_LOG_ERROR("Expected a discrete time bound at boundedUntilFormula but got" << f << "."); + return false; + } + } + } else if(objective.originalFormula->isRewardOperatorFormula()){ + storm::logic::Formula const& f = objective.originalFormula->asRewardOperatorFormula(); + if(f.isCumulativeRewardFormula()){ + if(f.asCumulativeRewardFormula().hasDiscreteTimeBound()){ + objective.stepBound = f.asCumulativeRewardFormula().getDiscreteTimeBound(); + } else { + STORM_LOG_ERROR("Expected a discrete time bound at cumulativeRewardFormula but got" << f << "."); + return false; + } + } + } else { + STORM_LOG_ERROR("Expected a Probability or Reward OperatorFormula but got " << *objective.originalFormula << "."); + return false; + } + return true; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::setWhetherNegativeRewardsAreConsidered(Information& info) { + // Negative Rewards are considered whenever there is an unbounded reward objective that requires to minimize. + // If there is no unbounded reward objective, we make a majority vote. + uint_fast64_t numOfMinimizingObjectives = 0; + for(auto const& obj : info.getObjectives()){ + if(obj.originalFormula->isRewardOperatorFormula() && !obj.stepBound){ + info.setNegativeRewardsConsidered(obj.originalFormulaMinimizes); + return true; + } + numOfMinimizingObjectives += obj.originalFormulaMinimizes ? 1 : 0; + } + // Reaching this point means that we make a majority vote + info.setNegativeRewardsConsidered(numOfMinimizingObjectives*2 > info.getObjectives().size()); + return true; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::ProbabilityOperatorFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective) { + // Check if we need to complement the property, e.g., P<0.3 [ F "a" ] ---> P >=0.7 [ G !"a" ] + // This is the case if the formula requires to minimize and positive rewards are considered or vice versa + if(info.areNegativeRewardsConsidered() != currentObjective.originalFormulaMinimizes){ + STORM_LOG_ERROR("Inverting of properties not yet supported"); + //TODO + return false; + } + + bool success = false; + // Invoke preprocessing for subformula + if(formula.getSubformula().isUntilFormula()){ + success = preprocess(formula.getSubformula().asUntilFormula(), info, currentObjective); + } else if(formula.getSubformula().isBoundedUntilFormula()){ + success = preprocess(formula.getSubformula().asBoundedUntilFormula(), info, currentObjective); + } else if(formula.getSubformula().isGloballyFormula()){ + success = preprocess(formula.getSubformula().asGloballyFormula(), info, currentObjective); + } else if(formula.getSubformula().isEventuallyFormula()){ + success = preprocess(formula.getSubformula().asEventuallyFormula(), info, currentObjective); + } + STORM_LOG_ERROR_COND(success, "No implementation for the subformula of " << formula << "."); + + return success; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::RewardOperatorFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective) { + // Make sure that our decision for negative rewards is consistent with the formula + if(info.areNegativeRewardsConsidered() != currentObjective.originalFormulaMinimizes){ + STORM_LOG_ERROR("Decided to consider " << (info.areNegativeRewardsConsidered() ? "negative" : "non-negative") << "rewards, but the formula " << formula << (currentObjective.originalFormulaMinimizes ? " minimizes" : "maximizes") << ". Reward objectives should either all minimize or all maximize."); + return false; + } + + // Check if the reward model is uniquely specified + if((formula.hasRewardModelName() && info.getModel().hasRewardModel(formula.getRewardModelName())) + || info.getModel().hasUniqueRewardModel()){ + STORM_LOG_ERROR("The reward model is not unique and the formula " << formula << " does not specify a reward model."); + return false; + } + + bool success = false; + // Invoke preprocessing for subformula + if(formula.getSubformula().isEventuallyFormula()){ + success = preprocess(formula.getSubformula().asEventuallyFormula(), info, currentObjective, formula.getOptionalRewardModelName()); + } else if(formula.getSubformula().isCumulativeRewardFormula()) { + success = preprocess(formula.getSubformula().asCumulativeRewardFormula(), info, currentObjective, formula.getOptionalRewardModelName()); + } + STORM_LOG_ERROR_COND(success, "No implementation for the subformula of " << formula << "."); + + return success; + + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::UntilFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective) { + bool success = false; + CheckTask phiTask(formula.getLeftSubformula()); + CheckTask psiTask(formula.getRightSubformula()); + storm::modelchecker::SparsePropositionalModelChecker mc(info.getModel()); + success = mc.canHandle(phiTask) && mc.canHandle(psiTask); + STORM_LOG_ERROR_COND(success, "The subformulas of " << formula << " should be propositional."); + storm::storage::BitVector phiStates = mc.check(phiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector psiStates = mc.check(psiTask)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + + // modelUnfolder(info.model, (~phiStates) | psiStates) + // info.model = modelUnfolder.info() + // build info.stateMapping from modelUnfolder.stateMapping + // build stateaction reward vector + // insert it in the model information + + // TODO + + return success; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::BoundedUntilFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective) { + return preprocess(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), info, currentObjective); + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::GloballyFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective) { + //TODO + STORM_LOG_ERROR("Globally not yet implemented"); + return false; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::EventuallyFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective, boost::optional const& optionalRewardModelName) { + if(formula.isReachabilityProbabilityFormula()){ + return preprocess(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), info, currentObjective); + } + if (!formula.isReachabilityRewardFormula()){ + STORM_LOG_ERROR("The formula " << formula << " neither considers reachability Probabilities nor reachability rewards"); + return false; + } + //TODO + STORM_LOG_ERROR("Rewards not yet implemented"); + return false; + } + + template + bool SparseMdpMultiObjectivePreprocessingHelper::preprocess(storm::logic::CumulativeRewardFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective, boost::optional const& optionalRewardModelName) { + //TODO + STORM_LOG_ERROR("Rewards not yet implemented"); + return false; + } + + + template class SparseMdpMultiObjectivePreprocessingHelper>; + + + } + } +} diff --git a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h new file mode 100644 index 000000000..a09939ee6 --- /dev/null +++ b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectivePreprocessingHelper.h @@ -0,0 +1,62 @@ +#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEPREPROCESSINGHELPER_H_ +#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEPREPROCESSINGHELPER_H_ + +#include "src/logic/Formulas.h" +#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h" +#include "src/storage/BitVector.h" + +namespace storm { + namespace modelchecker { + + + namespace helper { + + /* + * Helper Class to invoke the necessary preprocessing for multi objective model checking + */ + template + class SparseMdpMultiObjectivePreprocessingHelper { + public: + typedef typename SparseMdpModelType::ValueType ValueType; + typedef typename SparseMdpModelType::RewardModelType RewardModelType; + typedef SparseMultiObjectiveModelCheckerInformation Information; + + /*! + * Preprocesses the given model w.r.t. the given formulas. + * @param originalModel The considered model + * @param originalFormula the considered formula. The subformulas should only contain one OperatorFormula at top level, i.e., the formula is simple. + */ + static Information preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseMdpModelType originalModel); + + private: + + static bool gatherObjectiveInformation(storm::logic::MultiObjectiveFormula const& formula, Information& info); + static bool setStepBoundOfObjective(typename Information::ObjectiveInformation& currentObjective); + static bool setWhetherNegativeRewardsAreConsidered(Information& info); + + /*! + * Apply the neccessary preprocessing for the given formula. + * @param formula the current (sub)formula + * @param info the current state of the preprocessing. + * @return true iff there was no error + */ + // State formulas (will transform the formula and the reward model) + static bool preprocess(storm::logic::ProbabilityOperatorFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective); + static bool preprocess(storm::logic::RewardOperatorFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective); + + // Path formulas (will transform the model) + static bool preprocess(storm::logic::UntilFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective); + static bool preprocess(storm::logic::BoundedUntilFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective); + static bool preprocess(storm::logic::GloballyFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective); + static bool preprocess(storm::logic::EventuallyFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective, boost::optional const& optionalRewardModelName = boost::none); + static bool preprocess(storm::logic::CumulativeRewardFormula const& formula, Information& info, typename Information::ObjectiveInformation& currentObjective, boost::optional const& optionalRewardModelName = boost::none); + + static storm::storage::BitVector checkPropositionalFormula(storm::logic::Formula propFormula, SparseMdpModelType const& model); + + }; + + } + } +} + +#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEPREPROCESSINGHELPER_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h new file mode 100644 index 000000000..41e1840c4 --- /dev/null +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerInformation.h @@ -0,0 +1,83 @@ +#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEMODELCHECKERINFORMATION_H_ +#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEMODELCHECKERINFORMATION_H_ + +#include +#include + +#include "src/logic/Formulas.h" + +namespace storm { + namespace modelchecker { + + + namespace helper { + + template + class SparseMultiObjectiveModelCheckerInformation { + public : + + typedef typename SparseModelType::ValueType ValueType; + typedef typename SparseModelType::RewardModelType RewardModelType; + + struct ObjectiveInformation { + std::shared_ptr originalFormula; + bool originalFormulaMinimizes; + boost::optional threshold; + std::string rewardModelName; + boost::optional stepBound; + }; + + + SparseMultiObjectiveModelCheckerInformation(SparseModelType const& model) : model(model) { + //Intentionally left empty + } + + SparseMultiObjectiveModelCheckerInformation(SparseModelType && model) : model(model) { + //Intentionally left empty + } + + SparseModelType& getModel(){ + return model; + } + SparseModelType const& getModel() const { + return model; + } + + std::vector& getNewToOldStateMapping(){ + return newToOldStateMapping; + } + std::vectorconst& getNewToOldStateMapping() const{ + return newToOldStateMapping; + } + + bool areNegativeRewardsConsidered() { + return negativeRewardsConsidered; + } + + void setNegativeRewardsConsidered(bool value){ + negativeRewardsConsidered = value; + } + + std::vector& getObjectives() { + return objectives; + } + std::vectorconst& getObjectives() const { + return objectives; + } + + + private: + SparseModelType model; + std::vector newToOldStateMapping; + bool negativeRewardsConsidered; + + std::vector objectives; + + + + }; + } + } +} + +#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEMODELCHECKERINFORMATION_H_ */ diff --git a/src/utility/storm.h b/src/utility/storm.h index ce213cf08..a11fe2191 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -66,6 +66,7 @@ #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h" #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" +#include "src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -301,13 +302,19 @@ namespace storm { if (storm::settings::getModule().isCudaSet()) { storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker modelchecker(*mdp); result = modelchecker.check(task); - } else { - storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); + } else { +#endif + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); + if(modelchecker.canHandle(task)){ result = modelchecker.check(task); + } else { + storm::modelchecker::SparseMdpMultiObjectiveModelChecker> modelchecker2(*mdp); + if(modelchecker2.canHandle(task)){ + result = modelchecker2.check(task); + } } -#else - storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); - result = modelchecker.check(task); +#ifdef STORM_HAVE_CUDA + } #endif } else if (model->getType() == storm::models::ModelType::Ctmc) { std::shared_ptr> ctmc = model->template as>(); diff --git a/test/functional/logic/FragmentCheckerTest.cpp b/test/functional/logic/FragmentCheckerTest.cpp index 0280844d3..246db82c9 100644 --- a/test/functional/logic/FragmentCheckerTest.cpp +++ b/test/functional/logic/FragmentCheckerTest.cpp @@ -130,3 +130,43 @@ TEST(FragmentCheckerTest, Csrl) { ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); } + +TEST(FragmentCheckerTest, MultiObjective) { + storm::logic::FragmentChecker checker; + storm::logic::FragmentSpecification multiobjective = storm::logic::multiObjective().setNestedOperatorsInsideMultiObjectiveFormulasAllowed(true); + + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula; + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C<=3]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]")); + EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C<=3], P<0.6 [F \"label\"] & \"label\" & R<=4[F \"label\"])")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(P=? [F P<0.5 [F \"label\"]], \"label\" )")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(P=? [F P<0.5 [F \"label\"]], multi(\"label\", \"label\"))")); + EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); + + multiobjective.setNestedOperatorsInsideMultiObjectiveFormulasAllowed(false); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(P=? [F P<0.5 [F \"label\"]], \"label\" )")); + EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); + +}