srf_pbes.h File Reference

add your file description here. More...

Go to the source code of this file.

Classes
class	mcrl2::pbes_system::detail::pre_srf_summand< allow_ce >
class	mcrl2::pbes_system::detail::pre_srf_equation< allow_ce >
struct	mcrl2::pbes_system::detail::srf_or_traverser< allow_ce >
struct	mcrl2::pbes_system::detail::srf_and_traverser< allow_ce >
class	mcrl2::pbes_system::detail::pre_srf_pbes< allow_ce >

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

Typedefs
using	mcrl2::pbes_system::srf_summand = detail::pre_srf_summand< false >
using	mcrl2::pbes_system::srf_equation = detail::pre_srf_equation< false >
using	mcrl2::pbes_system::srf_pbes = detail::pre_srf_pbes< false >
	This is a PBES in SRF format.
using	mcrl2::pbes_system::srf_pbes_with_ce = detail::pre_srf_pbes< true >

Functions
pbes_expression	mcrl2::pbes_system::detail::make_not (const pbes_expression &x)
template<typename Iterator >
pbes_expression	mcrl2::pbes_system::detail::make_conjunction (Iterator first, Iterator last)
template<typename Iterator >
pbes_expression	mcrl2::pbes_system::detail::make_disjunction (Iterator first, Iterator last)
pbes_expression	mcrl2::pbes_system::detail::distribute_not_over_and (const pbes_expression &x)
	Assuming that x is of the form (x1 && x2 && ... xn), generates expression !x1 || !x2 || ... !xn.
template<bool allow_ce>
std::ostream &	mcrl2::pbes_system::detail::operator<< (std::ostream &out, const pre_srf_summand< allow_ce > &summand)
template<bool allow_ce>
std::ostream &	mcrl2::pbes_system::detail::operator<< (std::ostream &out, const pre_srf_equation< allow_ce > &eqn)
template<bool allow_ce>
std::vector< pre_srf_summand< allow_ce > >	mcrl2::pbes_system::detail::srf_or (const pbes_expression &phi, std::deque< pbes_equation > &equations, const pbes_equation &eqn, const data::variable_list &V, data::set_identifier_generator &id_generator, const core::identifier_string &X_true, const core::identifier_string &X_false, std::vector< pre_srf_equation< allow_ce > > &result, bool merge_simple_expressions)
template<bool allow_ce>
std::vector< pre_srf_summand< allow_ce > >	mcrl2::pbes_system::detail::srf_and (const pbes_expression &phi, std::deque< pbes_equation > &equations, const pbes_equation &eqn, const data::variable_list &V, data::set_identifier_generator &id_generator, const core::identifier_string &X_true, const core::identifier_string &X_false, std::vector< pre_srf_equation< allow_ce > > &result, bool merge_simple_expressions)
bool	mcrl2::pbes_system::detail::is_conjunctive (const pbes_expression &phi, bool allow_ce)
template<bool allow_ce>
detail::pre_srf_pbes< allow_ce >	mcrl2::pbes_system::detail::pbes2pre_srf (const pbes &p, bool merge_simple_expressions=true)
	Converts a PBES into standard recursive form.
srf_pbes	mcrl2::pbes_system::pre_srf2srfpbes (const srf_pbes_with_ce &p)
	Converts a pre-SRF PBES into standard recursive form. Note that the counter example information of the pre_srf_pbes is removed since otherwise the result is not in SRF.
srf_pbes_with_ce	mcrl2::pbes_system::pbes2pre_srf (const pbes &p, bool merge_simple_expressions=true)
	Converts a PBES into pre standard recursive form.
srf_pbes	mcrl2::pbes_system::pbes2srf (const pbes &p, bool merge_simple_expressions=true)
	Converts a PBES into standard recursive form.
bool	mcrl2::is_srf (const pbes_system::pbes &pbes, bool merge_simple_expressions=true)

Detailed Description

add your file description here.

Definition in file srf_pbes.h.