mcrl2::pres_system::algorithms Namespace Reference

Functions
void	remove_parameters (pres &x, const std::set< data::variable > &to_be_removed)
	Removes parameters from propositional variable instantiations in a pres expression.
void	remove_parameters (pres &x, const std::map< core::identifier_string, std::vector< std::size_t > > &to_be_removed)
	Removes parameters from propositional variable instantiations in a pres expression.
void	normalize (pres &x)
	The function normalize brings (embedded) pres expressions into positive normal form, i.e. a formula without any occurrences of ! or =>.
bool	is_normalized (const pres &x)
	Checks if a PRES is normalized.
void	instantiate_global_variables (pres &p)
	Attempts to eliminate the free variables of a PRES, by substituting a constant value for them. If no constant value is found for one of the variables, an exception is thrown.
void	presinst_finite (pres &p, data::rewrite_strategy rewrite_strategy, const std::string &finite_parameter_selection)
	Apply finite instantiation to the given PRES.
bool	is_res (const pres &x)
	Returns true if a PRES is in RES form.
std::string	print_removed_equations (const std::vector< propositional_variable > &removed)
	Print removed equations.
std::vector< propositional_variable >	remove_unreachable_variables (pres &p)
	Removes equations that are not (syntactically) reachable from the initial state of a PRES.
std::set< data::variable >	significant_variables (const pres_expression &x)
	Returns the significant variables of a pres expression.

Function Documentation

instantiate_global_variables()

void mcrl2::pres_system::algorithms::instantiate_global_variables

(

pres &

p

)

Attempts to eliminate the free variables of a PRES, by substituting a constant value for them. If no constant value is found for one of the variables, an exception is thrown.

Definition at line 68 of file pres.cpp.

is_normalized()

bool mcrl2::pres_system::algorithms::is_normalized

(

const pres &

x

)

Checks if a PRES is normalized.

Returns

True if the PRES is normalized

Definition at line 48 of file algorithms.cpp.

is_res()

bool mcrl2::pres_system::algorithms::is_res

(

const pres &

x

)

Returns true if a PRES is in RES form.

Parameters

x

a PRES

Definition at line 73 of file pres.cpp.

normalize()

void mcrl2::pres_system::algorithms::normalize

(

pres &

x

)

The function normalize brings (embedded) pres expressions into positive normal form, i.e. a formula without any occurrences of ! or =>.

Parameters

x	an object containing pres expressions

Definition at line 36 of file algorithms.cpp.

presinst_finite()

void mcrl2::pres_system::algorithms::presinst_finite	(	pres &	p,
		data::rewrite_strategy	rewrite_strategy,
		const std::string &	finite_parameter_selection
	)

Apply finite instantiation to the given PRES.

Definition at line 53 of file algorithms.cpp.

print_removed_equations()

std::string mcrl2::pres_system::algorithms::print_removed_equations

(

const std::vector< propositional_variable > &

removed

)

Print removed equations.

Definition at line 58 of file algorithms.cpp.

remove_parameters() [1/2]

void mcrl2::pres_system::algorithms::remove_parameters	(	pres &	x,
		const std::map< core::identifier_string, std::vector< std::size_t > > &	to_be_removed
	)

Removes parameters from propositional variable instantiations in a pres expression.

Parameters

x	A PRES library object that does not derive from atermpp::aterm
to_be_removed	A mapping that maps propositional variable names to indices of parameters that are removed

Returns

The expression x with parameters removed according to the mapping to_be_removed

Definition at line 31 of file algorithms.cpp.

remove_parameters() [2/2]

void mcrl2::pres_system::algorithms::remove_parameters	(	pres &	x,
		const std::set< data::variable > &	to_be_removed
	)

Removes parameters from propositional variable instantiations in a pres expression.

Parameters

x	A PRES library object that does not derive from atermpp::aterm
to_be_removed	A set of parameters that are to be removed

Returns

The expression x with parameters removed according to the mapping to_be_removed

Definition at line 26 of file algorithms.cpp.

remove_unreachable_variables()

std::vector< propositional_variable > mcrl2::pres_system::algorithms::remove_unreachable_variables

(

pres &

p

)

Removes equations that are not (syntactically) reachable from the initial state of a PRES.

Returns

The removed variables

Definition at line 63 of file algorithms.cpp.

significant_variables()

std::set< data::variable > mcrl2::pres_system::algorithms::significant_variables

(

const pres_expression &

x

)

Returns the significant variables of a pres expression.

Definition at line 68 of file algorithms.cpp.