algorithms.cpp File Reference

Go to the source code of this file.

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace	mcrl2::pbes_system
	The main namespace for the PBES library.
namespace	mcrl2::pbes_system::algorithms

Functions
void	mcrl2::pbes_system::algorithms::remove_parameters (pbes &x, const std::set< data::variable > &to_be_removed)
	Removes parameters from propositional variable instantiations in a pbes expression.
void	mcrl2::pbes_system::algorithms::remove_parameters (pbes &x, const std::map< core::identifier_string, std::vector< std::size_t > > &to_be_removed)
	Removes parameters from propositional variable instantiations in a pbes expression.
void	mcrl2::pbes_system::algorithms::normalize (pbes &x)
	The function normalize brings (embedded) pbes expressions into positive normal form, i.e. a formula without any occurrences of ! or =>.
bool	mcrl2::pbes_system::algorithms::is_normalized (const pbes &x)
	Checks if a PBEs is normalized.
void	mcrl2::pbes_system::algorithms::pbesinst_finite (pbes &p, data::rewrite_strategy rewrite_strategy, const std::string &finite_parameter_selection)
	Apply finite instantiation to the given PBES.
std::string	mcrl2::pbes_system::algorithms::print_removed_equations (const std::vector< propositional_variable > &removed)
	Print removed equations.
std::vector< propositional_variable >	mcrl2::pbes_system::algorithms::remove_unreachable_variables (pbes &p)
	Removes equations that are not (syntactically) reachable from the initial state of a PBES.
std::set< data::variable >	mcrl2::pbes_system::algorithms::significant_variables (const pbes_expression &x)
	Returns the significant variables of a pbes expression.