#include <IntegerVariable.h>

Inheritance diagram for storm::prism::IntegerVariable:

[legend]

Collaboration diagram for storm::prism::IntegerVariable:

[legend]

Public Member Functions
	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)
	Creates an integer variable with the given initial value expression.

bool	hasLowerBoundExpression () const

storm::expressions::Expression const &	getLowerBoundExpression () const
	Retrieves an expression defining the lower bound for this integer variable.

bool	hasUpperBoundExpression () const

storm::expressions::Expression const &	getUpperBoundExpression () const
	Retrieves an expression defining the upper bound for this integer variable.

storm::expressions::Expression	getRangeExpression () const
	Retrieves an expression characterizing the legal range of the variable.

IntegerVariable	substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
	Substitutes all identifiers in the boolean variable according to the given map.

IntegerVariable	substituteNonStandardPredicates () const

virtual void	createMissingInitialValue () override
	Equips the variable with an initial value based on its type if not initial value is present.

Public Member Functions inherited from storm::prism::Variable
	Variable (Variable const &otherVariable)=default

Variable &	operator= (Variable const &otherVariable)=default

	Variable (Variable &&otherVariable)=default

Variable &	operator= (Variable &&otherVariable)=default

virtual	~Variable ()=default

std::string const &	getName () const
	Retrieves the name of the variable.

bool	hasInitialValue () const
	Retrieves whether the variable has an initial value.

storm::expressions::Expression const &	getInitialValueExpression () const
	Retrieves the expression defining the initial value of the variable.

void	setInitialValueExpression (storm::expressions::Expression const &initialValueExpression)
	Sets the expression defining the initial value of the variable.

storm::expressions::Variable const &	getExpressionVariable () const
	Retrieves the expression variable associated with this variable.

storm::expressions::Expression	getExpression () const
	Retrieves the expression associated with this variable.

bool	isObservable () const
	Retrieves whether the variable is observable.

Public Member Functions inherited from storm::prism::LocatedInformation
	LocatedInformation (std::string const &filename, uint_fast64_t lineNumber)
	Constructs a located information with the given filename and line number.

	LocatedInformation ()=default

	LocatedInformation (LocatedInformation const &other)=default

LocatedInformation &	operator= (LocatedInformation const &other)=default

	LocatedInformation (LocatedInformation &&other)=default

LocatedInformation &	operator= (LocatedInformation &&other)=default

std::string const &	getFilename () const
	Retrieves the name of the file in which the information was found.

void	setFilename (std::string const &filename)
	Sets the filename of this information.

uint_fast64_t	getLineNumber () const
	Retrieves the line number in which the information was found.

void	setLineNumber (uint_fast64_t lineNumber)
	Sets the line number of this information.

Friends
std::ostream &	operator<< (std::ostream &stream, IntegerVariable const &variable)

Additional Inherited Members
Protected Member Functions inherited from storm::prism::Variable
	Variable ()=default

	Variable (storm::expressions::Variable const &variable, storm::expressions::Expression const &initialValueExpression, bool observable=false, std::string const &filename="", uint_fast64_t lineNumber=0)
	Creates a variable with the given initial value.

	Variable (storm::expressions::ExpressionManager &manager, Variable const &oldVariable, std::string const &newName, std::map< storm::expressions::Variable, storm::expressions::Expression > const &renaming, bool observable=false, std::string const &filename="", uint_fast64_t lineNumber=0)
	Creates a copy of the given variable and performs the provided renaming.

Detailed Description

Definition at line 10 of file IntegerVariable.h.

Constructor & Destructor Documentation

◆ IntegerVariable() [1/4]

storm::prism::IntegerVariable::IntegerVariable ( )

default

◆ IntegerVariable() [2/4]

storm::prism::IntegerVariable::IntegerVariable ( IntegerVariable const & other )

default

◆ IntegerVariable() [3/4]

storm::prism::IntegerVariable::IntegerVariable ( IntegerVariable && other )

default

◆ IntegerVariable() [4/4]

storm::prism::IntegerVariable::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`
	)

Creates an integer variable with the given initial value expression.

Parameters

variable	The expression variable associated with this variable.
lowerBoundExpression	A constant expression defining the lower bound of the domain of the variable.
upperBoundExpression	A constant expression defining the upper bound of the domain of the variable.
initialValueExpression	A constant expression that defines the initial value of the variable.
filename	The filename in which the variable is defined.
lineNumber	The line number in which the variable is defined.

Definition at line 7 of file IntegerVariable.cpp.

Member Function Documentation

◆ createMissingInitialValue()

void storm::prism::IntegerVariable::createMissingInitialValue ( )

overridevirtual

Equips the variable with an initial value based on its type if not initial value is present.

Implements storm::prism::Variable.

Definition at line 71 of file IntegerVariable.cpp.

◆ getLowerBoundExpression()

storm::expressions::Expression const & storm::prism::IntegerVariable::getLowerBoundExpression ( ) const

Retrieves an expression defining the lower bound for this integer variable.

Precondition: A lower bound for this integer variable is defined

Returns: An expression defining the lower bound for this integer variable.

Definition at line 20 of file IntegerVariable.cpp.

◆ getRangeExpression()

storm::expressions::Expression storm::prism::IntegerVariable::getRangeExpression ( ) const

Retrieves an expression characterizing the legal range of the variable.

Only bounds that are defined will be considered in this expression. If neither a lower nor an upper bound is defined, this expression will be equivalent to true.

Returns: An expression characterizing the legal range of the variable.

Definition at line 36 of file IntegerVariable.cpp.

◆ getUpperBoundExpression()

storm::expressions::Expression const & storm::prism::IntegerVariable::getUpperBoundExpression ( ) const

Retrieves an expression defining the upper bound for this integer variable.

Precondition: An upper bound for this integer variable is defined

Returns: An expression defining the upper bound for this integer variable.

Definition at line 30 of file IntegerVariable.cpp.

◆ hasLowerBoundExpression()

bool storm::prism::IntegerVariable::hasLowerBoundExpression ( ) const

Returns: true if a lower bound for this integer variable is defined

Definition at line 16 of file IntegerVariable.cpp.

◆ hasUpperBoundExpression()

bool storm::prism::IntegerVariable::hasUpperBoundExpression ( ) const

Returns: true if an upper bound for this integer variable is defined

Definition at line 26 of file IntegerVariable.cpp.

◆ operator=() [1/2]

IntegerVariable & storm::prism::IntegerVariable::operator= ( IntegerVariable && other )

default

◆ operator=() [2/2]

IntegerVariable & storm::prism::IntegerVariable::operator= ( IntegerVariable const & other )

default

◆ substitute()

IntegerVariable storm::prism::IntegerVariable::substitute ( std::map< storm::expressions::Variable, storm::expressions::Expression > const & substitution ) const

Substitutes all identifiers in the boolean variable according to the given map.

Parameters

substitution The substitution to perform.

Returns: The resulting boolean variable.

Definition at line 52 of file IntegerVariable.cpp.

◆ substituteNonStandardPredicates()

IntegerVariable storm::prism::IntegerVariable::substituteNonStandardPredicates ( ) const

Definition at line 61 of file IntegerVariable.cpp.

Friends And Related Symbol Documentation

◆ operator<<

std::ostream & operator<<	(	std::ostream &	stream,
		IntegerVariable const &	variable
	)

friend

Definition at line 81 of file IntegerVariable.cpp.

The documentation for this class was generated from the following files:

src/storm/storage/prism/IntegerVariable.h
src/storm/storage/prism/IntegerVariable.cpp

Public Member Functions

Friends

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ IntegerVariable() [1/4]

◆ IntegerVariable() [2/4]

◆ IntegerVariable() [3/4]

◆ IntegerVariable() [4/4]

Member Function Documentation

◆ createMissingInitialValue()

◆ getLowerBoundExpression()

◆ getRangeExpression()

◆ getUpperBoundExpression()

◆ hasLowerBoundExpression()

◆ hasUpperBoundExpression()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ substitute()

◆ substituteNonStandardPredicates()

Friends And Related Symbol Documentation

◆ operator<<