IntegerVariable.h

Go to the documentation of this file.

#ifndef STORM_STORAGE_PRISM_INTEGERVARIABLE_H_
#define STORM_STORAGE_PRISM_INTEGERVARIABLE_H_
 
#include <map>
 
#include "storm/storage/prism/Variable.h"
 
namespace storm {
namespace prism {
class IntegerVariable : public Variable {
   public:
    // Create default implementations of constructors/assignment.
    IntegerVariable() = default;
    IntegerVariable(IntegerVariable const& other) = default;
    IntegerVariable& operator=(IntegerVariable const& other) = default;
    IntegerVariable(IntegerVariable&& other) = default;
    IntegerVariable& operator=(IntegerVariable&& other) = default;
 
    IntegerVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBoundExpression,
                    storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, bool observable,
                    std::string const& filename = "", uint_fast64_t lineNumber = 0);
 
    bool hasLowerBoundExpression() const;
 
    storm::expressions::Expression const& getLowerBoundExpression() const;
 
    bool hasUpperBoundExpression() const;
 
    storm::expressions::Expression const& getUpperBoundExpression() const;
 
    storm::expressions::Expression getRangeExpression() const;
 
    IntegerVariable substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
 
    IntegerVariable substituteNonStandardPredicates() const;
 
    virtual void createMissingInitialValue() override;
 
    friend std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable);
 
   private:
    // A constant expression that specifies the lower bound of the domain of the variable.
    storm::expressions::Expression lowerBoundExpression;
 
    // A constant expression that specifies the upper bound of the domain of the variable.
    storm::expressions::Expression upperBoundExpression;
};
 
}  // namespace prism
}  // namespace storm
 
#endif /* STORM_STORAGE_PRISM_INTEGERVARIABLE_H_ */