pbes.h File Reference

The class pbes. More...

Go to the source code of this file.

Classes
class	mcrl2::pbes_system::pbes
	parameterized boolean equation system More...

Namespaces
namespace	mcrl2
namespace	mcrl2::pbes_system
	The main namespace for the PBES library.

Functions
void	mcrl2::pbes_system::complete_data_specification (pbes &p)
	Adds all sorts that appear in the PBES p to the data specification of p.
void	mcrl2::pbes_system::normalize_sorts (pbes_system::pbes &x, const data::sort_specification &)
void	mcrl2::pbes_system::translate_user_notation (pbes_system::pbes &x)
std::set< data::sort_expression >	mcrl2::pbes_system::find_sort_expressions (const pbes_system::pbes &x)
std::set< data::variable >	mcrl2::pbes_system::find_all_variables (const pbes_system::pbes &x)
std::set< data::variable >	mcrl2::pbes_system::find_free_variables (const pbes_system::pbes &x)
std::set< data::function_symbol >	mcrl2::pbes_system::find_function_symbols (const pbes_system::pbes &x)
bool	mcrl2::pbes_system::is_well_typed_equation (const pbes_equation &eqn, const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const data::data_specification &data_spec)
bool	mcrl2::pbes_system::is_well_typed_pbes (const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const std::set< data::variable > &occurring_global_variables, const std::set< propositional_variable > &declared_variables, const std::set< propositional_variable_instantiation > &occ, const propositional_variable_instantiation &init, const data::data_specification &data_spec)
atermpp::aterm	mcrl2::pbes_system::pbes_to_aterm (const pbes &p)
	Conversion to atermappl.
std::string	mcrl2::pbes_system::pp (const pbes_system::pbes &x, bool arg0)
std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const pbes &x)
bool	mcrl2::pbes_system::operator== (const pbes &p1, const pbes &p2)
	Equality operator on PBESs.

Detailed Description

The class pbes.

Definition in file pbes.h.