mcrl2/pbes/srf_pbes.h

Include file:

#include "mcrl2/pbes/srf_pbes.h"

add your file description here.

Classes

• mcrl2::pbes_system::detail::srf_and_traverser
• mcrl2::pbes_system::srf_equation
• mcrl2::pbes_system::detail::srf_or_traverser
• mcrl2::pbes_system::srf_pbes
• mcrl2::pbes_system::srf_summand

Functions

std::ostream &mcrl2::pbes_system::operator<<(std::ostream &out, const srf_equation &eqn)

std::ostream &mcrl2::pbes_system::operator<<(std::ostream &out, const srf_summand &summand)

srf_pbes mcrl2::pbes_system::pbes2srf(const pbes &p)

Converts a PBES into standard recursive form.

Pre: The pbes p must be normalized

Functions

bool mcrl2::pbes_system::detail::is_conjunctive(const pbes_expression &phi)

pbes_expression mcrl2::pbes_system::detail::make_not(const pbes_expression &x)

std::vector<srf_summand> 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<srf_equation> &result)

std::vector<srf_summand> 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<srf_equation> &result)