Dimension.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
#include <cstdint>
#include <memory>
#include <string>
 
#include "storm/logic/Formula.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/storage/BitVector.h"
 
namespace storm {
namespace modelchecker {
namespace helper {
namespace rewardbounded {
 
enum class DimensionBoundType {
    Unbounded,          // i.e., >=0 or <=B where B approaches infinity
    UpperBound,         // i.e., <=B where B is either a constant or a variable
    LowerBound,         // i.e., >B, where B is either a constant or a variable
    LowerBoundInfinity  // i.e., >B, where B approaches infinity
};
 
template<typename ValueType>
struct Dimension {
    std::shared_ptr<storm::logic::Formula const> formula;

    uint64_t objectiveIndex;

    boost::optional<std::string> memoryLabel;

    DimensionBoundType boundType;

    ValueType scalingFactor;

    storm::storage::BitVector dependentDimensions;

    boost::optional<uint64_t> maxValue;

    boost::optional<storm::solver::OptimizationDirection> optimizationDirection;
};
}  // namespace rewardbounded
}  // namespace helper
}  // namespace modelchecker
}  // namespace storm