#include <Property.h>

Public Member Functions
	Property ()=default

	Property (std::string const &name, std::shared_ptr< storm::logic::Formula const > const &formula, std::set< storm::expressions::Variable > const &undefinedConstants, std::string const &comment="")
	Constructs the property.

	Property (std::string const &name, FilterExpression const &fe, std::set< storm::expressions::Variable > const &undefinedConstants, std::string const &comment="")
	Constructs the property.

std::string const &	getName () const
	Get the provided name.

std::string const &	getComment () const
	Get the provided comment, if any.

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

Property	substitute (std::function< storm::expressions::Expression(storm::expressions::Expression const &)> const &substitutionFunction) const

Property	substituteLabels (std::map< std::string, std::string > const &labelSubstitution) const

Property	substituteRewardModelNames (std::map< std::string, std::string > const &rewardModelNameSubstitution) const

Property	substituteTranscendentalNumbers () const

Property	clone () const

FilterExpression const &	getFilter () const

std::string	asPrismSyntax () const

std::set< storm::expressions::Variable > const &	getUndefinedConstants () const

bool	containsUndefinedConstants () const

std::set< storm::expressions::Variable >	getUsedVariablesAndConstants () const

std::set< std::string >	getUsedLabels () const

void	gatherReferencedRewardModels (std::set< std::string > &rewardModelNames) const

std::shared_ptr< storm::logic::Formula const >	getRawFormula () const

Detailed Description

Definition at line 99 of file Property.h.

Constructor & Destructor Documentation

◆ Property() [1/3]

storm::jani::Property::Property ( )

default

◆ Property() [2/3]

storm::jani::Property::Property	(	std::string const &	name,
		std::shared_ptr< storm::logic::Formula const > const &	formula,
		std::set< storm::expressions::Variable > const &	undefinedConstants,
		std::string const &	comment = `""`
	)

Constructs the property.

Parameters

name	the name
formula	the formula representation
undefinedConstants	the undefined constants used in the property
comment	An optional comment

Definition at line 11 of file Property.cpp.

◆ Property() [3/3]

storm::jani::Property::Property	(	std::string const &	name,
		FilterExpression const &	fe,
		std::set< storm::expressions::Variable > const &	undefinedConstants,
		std::string const &	comment = `""`
	)

Constructs the property.

Parameters

name	the name
formula	the formula representation
comment	An optional comment

Definition at line 17 of file Property.cpp.

Member Function Documentation

◆ asPrismSyntax()

std::string storm::jani::Property::asPrismSyntax ( ) const

Definition at line 31 of file Property.cpp.

◆ clone()

Property storm::jani::Property::clone ( ) const

Definition at line 84 of file Property.cpp.

◆ containsUndefinedConstants()

bool storm::jani::Property::containsUndefinedConstants ( ) const

Definition at line 100 of file Property.cpp.

◆ gatherReferencedRewardModels()

void storm::jani::Property::gatherReferencedRewardModels ( std::set< std::string > & rewardModelNames ) const

Definition at line 124 of file Property.cpp.

◆ getComment()

std::string const & storm::jani::Property::getComment ( ) const

Get the provided comment, if any.

Returns: the comment

Definition at line 27 of file Property.cpp.

◆ getFilter()

FilterExpression const & storm::jani::Property::getFilter ( ) const

Definition at line 88 of file Property.cpp.

◆ getName()

std::string const & storm::jani::Property::getName ( ) const

Get the provided name.

Returns: the name

Definition at line 23 of file Property.cpp.

◆ getRawFormula()

std::shared_ptr< storm::logic::Formula const > storm::jani::Property::getRawFormula ( ) const

Definition at line 92 of file Property.cpp.

◆ getUndefinedConstants()

std::set< storm::expressions::Variable > const & storm::jani::Property::getUndefinedConstants ( ) const

Definition at line 96 of file Property.cpp.

◆ getUsedLabels()

std::set< std::string > storm::jani::Property::getUsedLabels ( ) const

Definition at line 111 of file Property.cpp.

◆ getUsedVariablesAndConstants()

std::set< storm::expressions::Variable > storm::jani::Property::getUsedVariablesAndConstants ( ) const

Definition at line 104 of file Property.cpp.

◆ substitute() [1/2]

Property storm::jani::Property::substitute ( std::function< storm::expressions::Expression(storm::expressions::Expression const &)> const & substitutionFunction ) const

Definition at line 64 of file Property.cpp.

◆ substitute() [2/2]

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

Definition at line 54 of file Property.cpp.

◆ substituteLabels()

Property storm::jani::Property::substituteLabels ( std::map< std::string, std::string > const & labelSubstitution ) const

Definition at line 72 of file Property.cpp.

◆ substituteRewardModelNames()

Property storm::jani::Property::substituteRewardModelNames ( std::map< std::string, std::string > const & rewardModelNameSubstitution ) const

Definition at line 76 of file Property.cpp.

◆ substituteTranscendentalNumbers()

Property storm::jani::Property::substituteTranscendentalNumbers ( ) const

Definition at line 80 of file Property.cpp.

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

src/storm/storage/jani/Property.h
src/storm/storage/jani/Property.cpp

Public Member Functions