#include <Formula.h>

Inheritance diagram for storm::prism::Formula:

Collaboration diagram for storm::prism::Formula:

Public Member Functions
	Formula (storm::expressions::Variable const &variable, storm::expressions::Expression const &expression, std::string const &filename="", uint_fast64_t lineNumber=0)
	Creates a formula with the given placeholder variable and expression.

	Formula (std::string const &name, storm::expressions::Expression const &expression, std::string const &filename="", uint_fast64_t lineNumber=0)
	Creates a formula with the given name and the assigning expression.

	Formula (std::string const &name, std::string const &filename="", uint_fast64_t lineNumber=0)
	Creates a formula with the given name.

	Formula ()=default

	Formula (Formula const &other)=default

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

	Formula (Formula &&other)=default

Formula &	operator= (Formula &&other)=default

std::string const &	getName () const
	Retrieves the name that is associated with this formula.

bool	hasExpressionVariable () const
	Retrieves wheter a placeholder variable is used in expressions to represent this formula.

storm::expressions::Variable const &	getExpressionVariable () const
	Retrieves the placeholder variable that is used in expressions to represent this formula.

storm::expressions::Expression const &	getExpression () const
	Retrieves the expression that is associated with this formula.

storm::expressions::Type const &	getType () const
	Retrieves the return type of the formula, i.e., the return-type of the defining expression.

Formula	substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const
	Substitutes all variables in the expression of the formula according to the given map.

Formula	substituteNonStandardPredicates () const

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, Formula const &formula)

Detailed Description

Definition at line 13 of file Formula.h.

Constructor & Destructor Documentation

◆ Formula() [1/6]

storm::prism::Formula::Formula	(	storm::expressions::Variable const &	variable,
		storm::expressions::Expression const &	expression,
		std::string const &	filename = `""`,
		uint_fast64_t	lineNumber = `0`
	)

Creates a formula with the given placeholder variable and expression.

Parameters

variable	The placeholder variable that is used in expressions to represent this formula.
expression	The expression associated with this formula.
filename	The filename in which the transition reward is defined.
lineNumber	The line number in which the transition reward is defined.

Definition at line 5 of file Formula.cpp.

◆ Formula() [2/6]

storm::prism::Formula::Formula	(	std::string const &	name,
		storm::expressions::Expression const &	expression,
		std::string const &	filename = `""`,
		uint_fast64_t	lineNumber = `0`
	)

Creates a formula with the given name and the assigning expression.

Parameters

name	the name of the formula.
expression	The expression associated with this formula.
filename	The filename in which the transition reward is defined.
lineNumber	The line number in which the transition reward is defined.

Definition at line 11 of file Formula.cpp.

◆ Formula() [3/6]

storm::prism::Formula::Formula	(	std::string const &	name,
		std::string const &	filename = `""`,
		uint_fast64_t	lineNumber = `0`
	)

Creates a formula with the given name.

Parameters

name	the name of the formula.
filename	The filename in which the transition reward is defined.
lineNumber	The line number in which the transition reward is defined.

Definition at line 16 of file Formula.cpp.

◆ Formula() [4/6]

storm::prism::Formula::Formula ( )

default

◆ Formula() [5/6]

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

default

◆ Formula() [6/6]

storm::prism::Formula::Formula ( Formula && other )

default

Member Function Documentation

◆ getExpression()

storm::expressions::Expression const & storm::prism::Formula::getExpression ( ) const

Retrieves the expression that is associated with this formula.

Returns: The expression that is associated with this formula.

Definition at line 32 of file Formula.cpp.

◆ getExpressionVariable()

storm::expressions::Variable const & storm::prism::Formula::getExpressionVariable ( ) const

Retrieves the placeholder variable that is used in expressions to represent this formula.

Returns: The placeholder variable that is used in expressions to represent this formula.

Definition at line 28 of file Formula.cpp.

◆ getName()

std::string const & storm::prism::Formula::getName ( ) const

Retrieves the name that is associated with this formula.

Returns: The name that is associated with this formula.

Definition at line 20 of file Formula.cpp.

◆ getType()

storm::expressions::Type const & storm::prism::Formula::getType ( ) const

Retrieves the return type of the formula, i.e., the return-type of the defining expression.

Returns: The return type of the formula.

Definition at line 36 of file Formula.cpp.

◆ hasExpressionVariable()

bool storm::prism::Formula::hasExpressionVariable ( ) const

Retrieves wheter a placeholder variable is used in expressions to represent this formula.

Definition at line 24 of file Formula.cpp.

◆ operator=() [1/2]

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

default

◆ operator=() [2/2]

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

default

◆ substitute()

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

Substitutes all variables in the expression of the formula according to the given map.

Will not substitute the placeholder variable (if given).

Parameters

substitution The substitution to perform.

Returns: The resulting formula.

Definition at line 42 of file Formula.cpp.

◆ substituteNonStandardPredicates()

Formula storm::prism::Formula::substituteNonStandardPredicates ( ) const

Definition at line 51 of file Formula.cpp.

Friends And Related Symbol Documentation

◆ operator<<

std::ostream & operator<<	(	std::ostream &	stream,
		Formula const &	formula
	)

friend

Definition at line 60 of file Formula.cpp.

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

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

Public Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

◆ Formula() [1/6]

◆ Formula() [2/6]

◆ Formula() [3/6]

◆ Formula() [4/6]

◆ Formula() [5/6]

◆ Formula() [6/6]

Member Function Documentation

◆ getExpression()

◆ getExpressionVariable()

◆ getName()

◆ getType()

◆ hasExpressionVariable()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ substitute()

◆ substituteNonStandardPredicates()

Friends And Related Symbol Documentation

◆ operator<<