diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h index 6598d5a85..b39023d34 100644 --- a/src/storm/modelchecker/CheckTask.h +++ b/src/storm/modelchecker/CheckTask.h @@ -10,6 +10,7 @@ #include "storm/solver/OptimizationDirection.h" #include "storm/logic/ComparisonType.h" #include "storm/logic/PlayerCoalition.h" +#include "storm/logic/ShieldExpression.h" #include "storm/modelchecker/hints/ModelCheckerHint.h" #include "storm/exceptions/InvalidOperationException.h" @@ -19,13 +20,13 @@ namespace storm { namespace logic { class Formula; } - + namespace modelchecker { - + enum class CheckType { Probabilities, Rewards }; - + /* * This class is used to customize the checking process of a formula. */ @@ -34,7 +35,7 @@ namespace storm { public: template friend class CheckTask; - + /*! * Creates a task object with the default options for the given formula. */ @@ -42,10 +43,10 @@ namespace storm { this->onlyInitialStatesRelevant = onlyInitialStatesRelevant; this->produceSchedulers = false; this->qualitative = false; - + updateOperatorInformation(); } - + /*! * 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. @@ -56,7 +57,7 @@ namespace storm { result.updateOperatorInformation(); return result; } - + /*! * If the currently specified formula is an OperatorFormula, this method updates the information that is given in the Operator formula. * Calling this method has no effect if the provided formula is not an operator formula. @@ -67,20 +68,20 @@ namespace storm { if (operatorFormula.hasOptimalityType()) { this->optimizationDirection = operatorFormula.getOptimalityType(); } - + if (operatorFormula.hasBound()) { this->bound = operatorFormula.getBound(); } - + if (operatorFormula.hasOptimalityType()) { this->optimizationDirection = operatorFormula.getOptimalityType(); } else if (operatorFormula.hasBound()) { this->optimizationDirection = operatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || operatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; } - + if (formula.get().isProbabilityOperatorFormula()) { storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.get().asProbabilityOperatorFormula(); - + if (probabilityOperatorFormula.hasBound()) { if (storm::utility::isZero(probabilityOperatorFormula.template getThresholdAs()) || storm::utility::isOne(probabilityOperatorFormula.template getThresholdAs())) { this->qualitative = true; @@ -89,7 +90,7 @@ namespace storm { } else if (formula.get().isRewardOperatorFormula()) { storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.get().asRewardOperatorFormula(); this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName(); - + if (rewardOperatorFormula.hasBound()) { if (storm::utility::isZero(rewardOperatorFormula.template getThresholdAs())) { this->qualitative = true; @@ -107,49 +108,49 @@ namespace storm { CheckTask convertValueType() const { return CheckTask(this->formula, this->optimizationDirection, this->playerCoalition, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint); } - + /*! * 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(); } - + /*! * Sets the optimization direction. */ void setOptimizationDirection(storm::OptimizationDirection const& dir) { optimizationDirection = dir; } - + /*! * Retrieves whether a player coalition was set. */ bool isPlayerCoalitionSet() const { return static_cast(playerCoalition); } - + /*! * Retrieves the player coalition (if set). */ storm::logic::PlayerCoalition const& getPlayerCoalition() const { return playerCoalition.get(); } - + /*! * Sets the player coalition. */ @@ -157,28 +158,28 @@ namespace storm { playerCoalition = coalition; return *this; } - + /*! * 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. */ @@ -186,14 +187,37 @@ namespace storm { this->onlyInitialStatesRelevant = value; return *this; } - + + /* + * TODO + */ + bool isShieldingTask() const { + return static_cast(shieldingExpression); + } + + /* + * TODO + */ + std::shared_ptr getShieldingExpression() const { + return shieldingExpression.get(); + } + + /* + * TODO + */ + CheckTask& setShieldingExpression(std::shared_ptr const& shieldingExpression) { + this->shieldingExpression = shieldingExpression; + this->produceSchedulers = true; + 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). */ @@ -201,14 +225,14 @@ namespace storm { STORM_LOG_THROW(!bound.get().threshold.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate threshold '" << bound.get().threshold << "' as it contains undefined constants."); return storm::utility::convertNumber(bound.get().threshold.evaluateAsRational()); } - + /*! * Retrieves the comparison type of the bound (if set). */ storm::logic::ComparisonType const& getBoundComparisonType() const { return bound.get().comparisonType; } - + /*! * Retrieves the bound (if set). */ @@ -238,46 +262,46 @@ namespace storm { void setQualitative(bool value) { qualitative = value; } - + /*! * Sets whether to produce schedulers (if supported). */ void setProduceSchedulers(bool produceSchedulers = true) { this->produceSchedulers = produceSchedulers; } - + /*! * Retrieves whether scheduler(s) are to be produced (if supported). */ bool isProduceSchedulersSet() const { return produceSchedulers; } - + /*! * sets a hint that might contain information that speeds up the modelchecking process (if supported by the model checker) */ void setHint(std::shared_ptr const& hint) { this->hint = hint; } - + /*! * Retrieves a hint that might contain information that speeds up the modelchecking process (if supported by the model checker) */ ModelCheckerHint const& getHint() const { return *hint; } - + ModelCheckerHint& getHint() { return *hint; } - + /*! * Conversion operator that strips the type of the formula. */ operator CheckTask() const { return this->substituteFormula(this->getFormula()); } - + private: /*! * Creates a task object with the given options. @@ -297,36 +321,42 @@ namespace storm { CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional playerCoalition, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional const& bound, bool qualitative, bool produceSchedulers, std::shared_ptr const& hint) : formula(formula), optimizationDirection(optimizationDirection), playerCoalition(playerCoalition), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers), hint(hint) { // 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 given coalitions of players will be assumed. boost::optional playerCoalition; // 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; + // If set to true, we will create the appropriate shield. + bool shieldingTask = false; + + // The according ShieldExpression. + boost::optional> shieldingExpression; + // The bound with which the 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, schedulers to achieve a value will be produced // if this flag is set. bool produceSchedulers; - + // A hint that might contain information that speeds up the modelchecking process (if supported by the model checker) std::shared_ptr hint; }; - + } }