Dimension.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
 
#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