SingleValueModelCheckerHelper.h

Go to the documentation of this file.

#pragma once
 
#include "ModelCheckerHelper.h"
 
#include "storm/logic/ComparisonType.h"
#include "storm/solver/OptimizationDirection.h"
 
namespace storm {
namespace modelchecker {
namespace helper {
 
template<typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
class SingleValueModelCheckerHelper : public ModelCheckerHelper<ValueType, ModelRepresentation> {
   public:
    SingleValueModelCheckerHelper();
 
    void setOptimizationDirection(storm::solver::OptimizationDirection const& direction);
 
    void clearOptimizationDirection();
 
    bool isOptimizationDirectionSet() const;
 
    storm::solver::OptimizationDirection const& getOptimizationDirection() const;
 
    bool minimize() const;
 
    bool maximize() const;
 
    boost::optional<storm::solver::OptimizationDirection> getOptionalOptimizationDirection() const;
 
    void setValueThreshold(storm::logic::ComparisonType const& comparisonType, ValueType const& thresholdValue);
 
    void clearValueThreshold();
 
    bool isValueThresholdSet() const;
 
    storm::logic::ComparisonType const& getValueThresholdComparisonType() const;
 
    ValueType const& getValueThresholdValue() const;
 
    void setProduceScheduler(bool value);
 
    bool isProduceSchedulerSet() const;
 
    void setQualitative(bool value);
 
    bool isQualitativeSet() const;
 
   private:
    boost::optional<storm::solver::OptimizationDirection> _optimizationDirection;
    boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> _valueThreshold;
    bool _produceScheduler;
    bool _isQualitativeSet;
};
}  // namespace helper
}  // namespace modelchecker
}  // namespace storm