CheckTask.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
#include <memory>
 
#include "storm/logic/Formulas.h"
#include "storm/utility/constants.h"
 
#include "storm/adapters/IntervalForward.h"
#include "storm/logic/ComparisonType.h"
#include "storm/logic/PlayerCoalition.h"
#include "storm/modelchecker/hints/ModelCheckerHint.h"
#include "storm/solver/UncertaintyResolutionMode.h"
 
#include "storm/exceptions/InvalidOperationException.h"
 
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.
 */
template<typename FormulaType = storm::logic::Formula, typename ValueType = double>
class CheckTask {
   public:
    template<typename OtherFormulaType, typename OtherValueType>
    friend class CheckTask;

    CheckTask(FormulaType const& formula, bool onlyInitialStatesRelevant = false, UncertaintyResolutionMode = UncertaintyResolutionMode::Unset)
        : formula(formula), hint(new ModelCheckerHint()) {
        this->onlyInitialStatesRelevant = onlyInitialStatesRelevant;
        this->produceSchedulers = false;
        this->qualitative = false;
        this->uncertaintyResolutionMode = UncertaintyResolutionMode::Unset;
 
        updateOperatorInformation();
    }

    template<typename NewFormulaType>
    CheckTask<NewFormulaType, ValueType> substituteFormula(NewFormulaType const& newFormula) const {
        CheckTask<NewFormulaType, ValueType> result(newFormula, this->optimizationDirection, this->playerCoalition, this->rewardModel,
                                                    this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint,
                                                    this->uncertaintyResolutionMode);
        result.updateOperatorInformation();
        return result;
    }

    void updateOperatorInformation() {
        if (formula.get().isOperatorFormula()) {
            storm::logic::OperatorFormula const& operatorFormula = formula.get().asOperatorFormula();
            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<ValueType>()) ||
                        storm::utility::isOne(probabilityOperatorFormula.template getThresholdAs<ValueType>())) {
                        this->qualitative = true;
                    }
                }
            } 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<ValueType>())) {
                        this->qualitative = true;
                    }
                }
            }
        }
    }

    CheckTask negate() const {
        CheckTask result(*this);
        if (isOptimizationDirectionSet()) {
            // switch from min to max and vice-versa
            result.setOptimizationDirection(invert(getOptimizationDirection()));
        }
 
        if (isBoundSet()) {
            // invert bound comparison type (retain strictness),
            // convert threshold to 1- threshold
            result.bound = storm::logic::Bound(storm::logic::invertPreserveStrictness(getBound().comparisonType), 1 - getBound().threshold);
        }
 
        return result;
    }

    template<typename NewValueType>
    CheckTask<FormulaType, NewValueType> convertValueType() const {
        return CheckTask<FormulaType, NewValueType>(this->formula, this->optimizationDirection, this->playerCoalition, this->rewardModel,
                                                    this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint,
                                                    this->uncertaintyResolutionMode);
    }

    FormulaType const& getFormula() const {
        return formula.get();
    }

    bool isOptimizationDirectionSet() const {
        return static_cast<bool>(optimizationDirection);
    }

    storm::OptimizationDirection const& getOptimizationDirection() const {
        return optimizationDirection.get();
    }

    void setOptimizationDirection(storm::OptimizationDirection const& dir) {
        optimizationDirection = dir;
    }

    bool isPlayerCoalitionSet() const {
        return static_cast<bool>(playerCoalition);
    }

    storm::logic::PlayerCoalition const& getPlayerCoalition() const {
        return playerCoalition.get();
    }

    CheckTask<FormulaType, ValueType>& setPlayerCoalition(storm::logic::PlayerCoalition const& coalition) {
        playerCoalition = coalition;
        return *this;
    }

    bool isRewardModelSet() const {
        return static_cast<bool>(rewardModel);
    }

    std::string const& getRewardModel() const {
        return rewardModel.get();
    }

    bool isOnlyInitialStatesRelevantSet() const {
        return onlyInitialStatesRelevant;
    }

    CheckTask<FormulaType, ValueType>& setOnlyInitialStatesRelevant(bool value = true) {
        this->onlyInitialStatesRelevant = value;
        return *this;
    }

    bool isBoundSet() const {
        return static_cast<bool>(bound);
    }

    ValueType getBoundThreshold() const {
        STORM_LOG_THROW(!bound.get().threshold.containsVariables(), storm::exceptions::InvalidOperationException,
                        "Cannot evaluate threshold '" << bound.get().threshold << "' as it contains undefined constants.");
        return bound.get().template evaluateThresholdAs<ValueType>();
    }

    storm::logic::ComparisonType const& getBoundComparisonType() const {
        return bound.get().comparisonType;
    }

    storm::logic::Bound const& getBound() const {
        return bound.get();
    }

    boost::optional<storm::logic::Bound> const& getOptionalBound() const {
        return bound;
    }

    bool isQualitativeSet() const {
        return qualitative;
    }

    void setQualitative(bool value) {
        qualitative = value;
    }

    void setProduceSchedulers(bool produceSchedulers = true) {
        this->produceSchedulers = produceSchedulers;
    }

    bool isProduceSchedulersSet() const {
        return produceSchedulers;
    }

    void setHint(std::shared_ptr<ModelCheckerHint> const& hint) {
        this->hint = hint;
    }

    ModelCheckerHint const& getHint() const {
        return *hint;
    }
 
    ModelCheckerHint& getHint() {
        return *hint;
    }

    UncertaintyResolutionMode getUncertaintyResolutionMode() const {
        return uncertaintyResolutionMode;
    }

    void setUncertaintyResolutionMode(UncertaintyResolutionMode uncertaintyResolutionMode) {
        this->uncertaintyResolutionMode = uncertaintyResolutionMode;
    }

    bool isUncertaintyResolutionModeSet() const {
        return isSet(this->uncertaintyResolutionMode);
    }

    operator CheckTask<storm::logic::Formula, ValueType>() const {
        return this->template substituteFormula<storm::logic::Formula>(this->getFormula());
    }
 
   private:
    CheckTask(std::reference_wrapper<FormulaType const> const& formula, boost::optional<storm::OptimizationDirection> const& optimizationDirection,
              boost::optional<storm::logic::PlayerCoalition> playerCoalition, boost::optional<std::string> const& rewardModel, bool onlyInitialStatesRelevant,
              boost::optional<storm::logic::Bound> const& bound, bool qualitative, bool produceSchedulers, std::shared_ptr<ModelCheckerHint> const& hint,
              UncertaintyResolutionMode uncertaintyResolutionMode)
        : formula(formula),
          optimizationDirection(optimizationDirection),
          playerCoalition(playerCoalition),
          rewardModel(rewardModel),
          onlyInitialStatesRelevant(onlyInitialStatesRelevant),
          bound(bound),
          qualitative(qualitative),
          produceSchedulers(produceSchedulers),
          hint(hint),
          uncertaintyResolutionMode(uncertaintyResolutionMode) {
        // Intentionally left empty.
    }
 
    // The formula that is to be checked.
    std::reference_wrapper<FormulaType const> formula;
 
    // If set, the probabilities will be minimized/maximized.
    boost::optional<storm::OptimizationDirection> optimizationDirection;
 
    // If set, the given coalitions of players will be assumed.
    boost::optional<storm::logic::PlayerCoalition> playerCoalition;
 
    // If set, the reward property has to be interpreted over this model.
    boost::optional<std::string> 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 states will be compared.
    boost::optional<storm::logic::Bound> 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<ModelCheckerHint> hint;
 
    // Whether uncertainty should be resolved be minimizing, maximizing, acting robust or cooperative.
    UncertaintyResolutionMode uncertaintyResolutionMode;
};
 
}  // namespace modelchecker
}  // namespace storm