Stores the following properties of a linear process specification: More...

#include <specification_property_map.h>

Inheritance diagram for mcrl2::lps::detail::specification_property_map< Specification >:

Public Member Functions
	specification_property_map (const std::string &text)
	Constructor. The strings may appear in a random order, and not all of them need to be present.

	specification_property_map (const Specification &spec)
	Constructor Initializes the specification_property_map with a linear process specification.

std::string	compare (const specification_property_map< Specification > &other) const

std::string	info () const
	Returns a textual overview of some properties of an LPS.

std::string	to_string () const
	Returns a string representation of the properties.

const std::map< std::string, std::string > &	data () const
	Returns the stored properties.

Protected Types
typedef data::detail::data_property_map< specification_property_map >	super

Protected Member Functions
std::string	print (const process::action_label &l) const

std::string	print (const process::action &a) const

std::string	print (const deadlock &x) const

std::string	print (const multi_action &x) const

std::string	print (const std::set< std::multiset< process::action_label > > &v) const

std::string	compare_property (std::string property, std::string x, std::string y) const

std::set< std::multiset< process::action_label > >	compute_used_multi_actions (const Specification &spec) const

std::set< process::action_label >	compute_used_action_labels (const Specification &spec) const

std::size_t	compute_tau_summand_count (const Specification &spec) const

std::set< data::variable >	compute_used_free_variables (const Specification &spec) const

template<typename Container >
std::set< core::identifier_string >	names (const Container &v) const
	Collects the names of the elements of the container. The name of element x is retrieved by x.name().

std::string	print (std::size_t n) const

std::string	print (std::string s) const

std::string	print (const core::identifier_string &s) const

std::string	print (const data::variable &v) const

template<typename Container >
std::string	print (const Container &v, typename atermpp::enable_if_container< Container >::type *=nullptr) const

template<typename Container >
std::string	print (const Container &v, bool print_separators, typename atermpp::enable_if_container< Container >::type *=nullptr) const

unsigned int	parse_unsigned_int (std::string const &text) const

std::set< std::string >	parse_set_string (std::string const &text) const

std::set< std::multiset< std::string > >	parse_set_multiset_string (std::string const &text) const

std::string	compare (const std::string &property, unsigned int x, unsigned int y) const
	Compares two integers, and returns a message if they are different. If if they are equal the empty string is returned.

template<typename T >
std::string	compare (const std::string &property, const std::set< T > &x, const std::set< T > &y) const
	Compares two sets and returns a string with the differences encountered. Elements present in the first one but not in the second are printed with a '+' in front of it, elements present in the seconde but not in the first one with a '-' in front of it. A value x of the type T is printed using print(x), so this operation must be defined. If no differences are found the empty string is returned.

std::string	compare (const data_property_map &other) const
	Compares this property map with another property map. The function compare_property must be defined properly for all available properties.

Protected Member Functions inherited from mcrl2::data::detail::data_property_map< Derived >
std::string	print (std::size_t n) const

std::string	print (std::string s) const

std::string	print (const core::identifier_string &s) const

std::string	print (const data::variable &v) const

template<typename Container >
std::string	print (const Container &v, typename atermpp::enable_if_container< Container >::type *=nullptr) const

template<typename Container >
std::string	print (const Container &v, bool print_separators, typename atermpp::enable_if_container< Container >::type *=nullptr) const

unsigned int	parse_unsigned_int (std::string const &text) const

std::set< std::string >	parse_set_string (std::string const &text) const

std::set< std::multiset< std::string > >	parse_set_multiset_string (std::string const &text) const

std::string	compare (const std::string &property, unsigned int x, unsigned int y) const
	Compares two integers, and returns a message if they are different. If if they are equal the empty string is returned.

template<typename T >
std::string	compare (const std::string &property, const std::set< T > &x, const std::set< T > &y) const
	Compares two sets and returns a string with the differences encountered. Elements present in the first one but not in the second are printed with a '+' in front of it, elements present in the seconde but not in the first one with a '-' in front of it. A value x of the type T is printed using print(x), so this operation must be defined. If no differences are found the empty string is returned.

std::string	compare_property (const std::string &property, const std::string &, const std::string &) const
	Compares two values x and y of a given property. This function should be redefined in derived classes.

unsigned int	max_key_length () const
	Returns the maximum length of the property names.

std::string	align (const std::string &s, unsigned int n) const

template<typename Container >
std::set< core::identifier_string >	names (const Container &v) const
	Collects the names of the elements of the container. The name of element x is retrieved by x.name().

	data_property_map ()
	Default constructor for derived types.

void	parse_text (const std::string &text)
	Initializes the property map with text containing lines in `KEY = VALUE` format.

	data_property_map (const std::string &text)
	The strings may appear in a random order, and not all of them need to be present.

std::string	to_string () const
	Returns a string representation of the properties.

const std::map< std::string, std::string > &	data () const
	Returns the stored properties.

std::string	operator[] (const std::string &key) const
	Returns the value corresponding to key. Throws an exception if the key is not found.

std::string	compare (const data_property_map &other) const
	Compares this property map with another property map. The function compare_property must be defined properly for all available properties.

Protected Attributes
std::map< std::string, std::string >	m_data
	Contains a normalized string representation of the properties.

Protected Attributes inherited from mcrl2::data::detail::data_property_map< Derived >
std::map< std::string, std::string >	m_data
	Contains a normalized string representation of the properties.

Friends
class	data::detail::data_property_map< specification_property_map< Specification > >

Additional Inherited Members
Static Protected Member Functions inherited from mcrl2::data::detail::data_property_map< Derived >
template<typename Container >
static std::string	add_separators (std::string const &c, typename std::enable_if< atermpp::is_set< Container >::value >::type *=nullptr)
	Add start/end separators for non-set container types.

template<typename Container >
static std::string	add_separators (std::string const &c, typename std::enable_if< !atermpp::is_set< Container >::value >::type *=0)
	Add start/end separators for set container types.

Detailed Description

template<typename Specification = specification>
class mcrl2::lps::detail::specification_property_map< Specification >

Stores the following properties of a linear process specification:

property	description	format
action_summand_count	The number of action summands	NUMBER
tau_summand_count	The number of tau summands	NUMBER
delta_summand_count	The number of delta/deadlock summands	NUMBER
declared_free_variables	The declared free variables	NAME:SORT; ... ; NAME:SORT
declared_free_variable_names	The names of the declared free variables	NAME; ... ; NAME
declared_variable_count	The number of declared free variables	NUMBER
used_free_variables	The used free variables	NAME:SORT; ... ; NAME:SORT
used_free_variables_names	The names of the used free variables	NAME; ... ; NAME
used_free_variable_count	The number of used free variables	NUMBER
process_parameters	The process parameters	NAME:SORT; ... ; NAME:SORT
process_parameter_names	The names of the process parameters	NAME; ... ; NAME
process_parameter_count	The number of process parameters	NUMBER
declared_action_labels	The names of the declared action labels	NAME; ... ; NAME
declared_action_label_count	The number of declared action labels	NUMBER
used_action_labels	The names of the used action labels	NAME; ... ; NAME
used_action_label_count	The number of used action labels	NUMBER
used_multi_actions	The used multi-actions (sets of label names)	{NAME,...,NAME}; ... ; {NAME,...,NAME}
used_multi_action_count	The number of used multi-actions	NUMBER

Definition at line 52 of file specification_property_map.h.

Member Typedef Documentation

◆ super

template<typename Specification = specification>

typedef data::detail::data_property_map<specification_property_map> mcrl2::lps::detail::specification_property_map< Specification >::super

protected

Definition at line 59 of file specification_property_map.h.

Constructor & Destructor Documentation

◆ specification_property_map() [1/2]

template<typename Specification = specification>

mcrl2::lps::detail::specification_property_map< Specification >::specification_property_map ( const std::string & text )

inline

Constructor. The strings may appear in a random order, and not all of them need to be present.

Definition at line 232 of file specification_property_map.h.

◆ specification_property_map() [2/2]

template<typename Specification = specification>

mcrl2::lps::detail::specification_property_map< Specification >::specification_property_map ( const Specification & spec )

inline

Constructor Initializes the specification_property_map with a linear process specification.

Definition at line 238 of file specification_property_map.h.

Member Function Documentation

◆ compare() [1/4]

template<typename Specification = specification>

std::string mcrl2::data::detail::data_property_map< Derived >::compare ( const data_property_map & other ) const

inlineprotected

Compares this property map with another property map. The function compare_property must be defined properly for all available properties.

Returns: A string describing the differences found.

Definition at line 286 of file data_property_map.h.

◆ compare() [2/4]

template<typename Specification = specification>

std::string mcrl2::lps::detail::specification_property_map< Specification >::compare ( const specification_property_map< Specification > & other ) const

inline

Definition at line 278 of file specification_property_map.h.

◆ compare() [3/4]

template<typename Specification = specification>

template<typename T >

std::string mcrl2::data::detail::data_property_map< Derived >::compare	(	const std::string &	property,
		const std::set< T > &	x,
		const std::set< T > &	y
	)		const

inlineprotected

Compares two sets and returns a string with the differences encountered. Elements present in the first one but not in the second are printed with a '+' in front of it, elements present in the seconde but not in the first one with a '-' in front of it. A value x of the type T is printed using print(x), so this operation must be defined. If no differences are found the empty string is returned.

Definition at line 150 of file data_property_map.h.

◆ compare() [4/4]

template<typename Specification = specification>

std::string mcrl2::data::detail::data_property_map< Derived >::compare	(	const std::string &	property,
		unsigned int	x,
		unsigned int	y
	)		const

inlineprotected

Compares two integers, and returns a message if they are different. If if they are equal the empty string is returned.

Definition at line 132 of file data_property_map.h.

◆ compare_property()

template<typename Specification = specification>

std::string mcrl2::lps::detail::specification_property_map< Specification >::compare_property	(	std::string	property,
		std::string	x,
		std::string	y
	)		const

inlineprotected

Definition at line 101 of file specification_property_map.h.

◆ compute_tau_summand_count()

template<typename Specification = specification>

std::size_t mcrl2::lps::detail::specification_property_map< Specification >::compute_tau_summand_count ( const Specification & spec ) const

inlineprotected

Definition at line 210 of file specification_property_map.h.

◆ compute_used_action_labels()

template<typename Specification = specification>

std::set< process::action_label > mcrl2::lps::detail::specification_property_map< Specification >::compute_used_action_labels ( const Specification & spec ) const

inlineprotected

Definition at line 197 of file specification_property_map.h.

◆ compute_used_free_variables()

template<typename Specification = specification>

std::set< data::variable > mcrl2::lps::detail::specification_property_map< Specification >::compute_used_free_variables ( const Specification & spec ) const

inlineprotected

Definition at line 224 of file specification_property_map.h.

◆ compute_used_multi_actions()

template<typename Specification = specification>

std::set< std::multiset< process::action_label > > mcrl2::lps::detail::specification_property_map< Specification >::compute_used_multi_actions ( const Specification & spec ) const

inlineprotected

Definition at line 182 of file specification_property_map.h.

◆ data()

template<typename Specification = specification>

const std::map< std::string, std::string > & mcrl2::data::detail::data_property_map< Derived >::data ( ) const

inline

Returns the stored properties.

Definition at line 265 of file data_property_map.h.

◆ info()

template<typename Specification = specification>

std::string mcrl2::lps::detail::specification_property_map< Specification >::info ( ) const

inline

Returns a textual overview of some properties of an LPS.

Definition at line 284 of file specification_property_map.h.

◆ names()

template<typename Specification = specification>

template<typename Container >

std::set< core::identifier_string > mcrl2::data::detail::data_property_map< Derived >::names ( const Container & v ) const

inlineprotected

Collects the names of the elements of the container. The name of element x is retrieved by x.name().

Definition at line 214 of file data_property_map.h.

◆ parse_set_multiset_string()

template<typename Specification = specification>

std::set< std::multiset< std::string > > mcrl2::data::detail::data_property_map< Derived >::parse_set_multiset_string ( std::string const & text ) const

inlineprotected

Definition at line 113 of file data_property_map.h.

◆ parse_set_string()

template<typename Specification = specification>

std::set< std::string > mcrl2::data::detail::data_property_map< Derived >::parse_set_string ( std::string const & text ) const

inlineprotected

Definition at line 106 of file data_property_map.h.

◆ parse_unsigned_int()

template<typename Specification = specification>

unsigned int mcrl2::data::detail::data_property_map< Derived >::parse_unsigned_int ( std::string const & text ) const

inlineprotected

Definition at line 101 of file data_property_map.h.

◆ print() [1/11]

template<typename Specification = specification>

template<typename Container >

std::string mcrl2::data::detail::data_property_map< Derived >::print	(	const Container &	v,
		bool	print_separators,
		typename atermpp::enable_if_container< Container >::type *	= `nullptr`
	)		const

inlineprotected

Definition at line 93 of file data_property_map.h.

◆ print() [2/11]

template<typename Specification = specification>

template<typename Container >

std::string mcrl2::data::detail::data_property_map< Derived >::print	(	const Container &	v,
		typename atermpp::enable_if_container< Container >::type *	= `nullptr`
	)		const

inlineprotected

Definition at line 80 of file data_property_map.h.

◆ print() [3/11]

template<typename Specification = specification>

std::string mcrl2::data::detail::data_property_map< Derived >::print ( const core::identifier_string & s ) const

inlineprotected

Definition at line 69 of file data_property_map.h.

◆ print() [4/11]

template<typename Specification = specification>

std::string mcrl2::data::detail::data_property_map< Derived >::print ( const data::variable & v ) const

inlineprotected

Definition at line 74 of file data_property_map.h.

◆ print() [5/11]

template<typename Specification = specification>

std::string mcrl2::lps::detail::specification_property_map< Specification >::print ( const deadlock & x ) const

inlineprotected

Definition at line 78 of file specification_property_map.h.

◆ print() [6/11]

template<typename Specification = specification>

std::string mcrl2::lps::detail::specification_property_map< Specification >::print ( const multi_action & x ) const

inlineprotected

Definition at line 83 of file specification_property_map.h.

◆ print() [7/11]

template<typename Specification = specification>

std::string mcrl2::lps::detail::specification_property_map< Specification >::print ( const process::action & a ) const

inlineprotected

Definition at line 73 of file specification_property_map.h.

◆ print() [8/11]

template<typename Specification = specification>

std::string mcrl2::lps::detail::specification_property_map< Specification >::print ( const process::action_label & l ) const

inlineprotected

Definition at line 68 of file specification_property_map.h.

◆ print() [9/11]

template<typename Specification = specification>

std::string mcrl2::lps::detail::specification_property_map< Specification >::print ( const std::set< std::multiset< process::action_label > > & v ) const

inlineprotected

Definition at line 88 of file specification_property_map.h.

◆ print() [10/11]

template<typename Specification = specification>

std::string mcrl2::data::detail::data_property_map< Derived >::print ( std::size_t n ) const

inlineprotected

Definition at line 57 of file data_property_map.h.

◆ print() [11/11]

template<typename Specification = specification>

std::string mcrl2::data::detail::data_property_map< Derived >::print ( std::string s ) const

inlineprotected

Definition at line 64 of file data_property_map.h.

◆ to_string()

template<typename Specification = specification>

std::string mcrl2::data::detail::data_property_map< Derived >::to_string ( ) const

inline

Returns a string representation of the properties.

Definition at line 253 of file data_property_map.h.

Friends And Related Symbol Documentation

◆ data::detail::data_property_map< specification_property_map< Specification > >

template<typename Specification = specification>

friend class data::detail::data_property_map< specification_property_map< Specification > >

friend

Definition at line 1 of file specification_property_map.h.

Member Data Documentation

◆ m_data

template<typename Specification = specification>

std::map<std::string, std::string> mcrl2::data::detail::data_property_map< Derived >::m_data

protected

Contains a normalized string representation of the properties.

Definition at line 52 of file data_property_map.h.

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

lps/include/mcrl2/lps/detail/specification_property_map.h

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Friends

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ super

Constructor & Destructor Documentation

◆ specification_property_map() [1/2]

◆ specification_property_map() [2/2]

Member Function Documentation

◆ compare() [1/4]

◆ compare() [2/4]

◆ compare() [3/4]

◆ compare() [4/4]

◆ compare_property()

◆ compute_tau_summand_count()

◆ compute_used_action_labels()

◆ compute_used_free_variables()

◆ compute_used_multi_actions()

◆ data()

◆ info()

◆ names()

◆ parse_set_multiset_string()

◆ parse_set_string()

◆ parse_unsigned_int()

◆ print() [1/11]

◆ print() [2/11]

◆ print() [3/11]

◆ print() [4/11]

◆ print() [5/11]

◆ print() [6/11]

◆ print() [7/11]

◆ print() [8/11]

◆ print() [9/11]

◆ print() [10/11]

◆ print() [11/11]

◆ to_string()

Friends And Related Symbol Documentation

◆ data::detail::data_property_map< specification_property_map< Specification > >

Member Data Documentation

◆ m_data