mcrl2/pbes/constelm.h

Include file:

#include "mcrl2/pbes/constelm.h"

The constelm algorithm.

Classes

• mcrl2::pbes_system::pbes_constelm_algorithm::edge
• mcrl2::pbes_system::detail::edge_condition_traverser
• mcrl2::pbes_system::detail::edge_details
• mcrl2::pbes_system::detail::edge_traverser_stack_elem
• mcrl2::pbes_system::pbes_constelm_algorithm
• mcrl2::pbes_system::detail::QPVI
• mcrl2::pbes_system::detail::quantified_variable
• mcrl2::pbes_system::pbes_constelm_algorithm::vertex

Functions

void mcrl2::pbes_system::constelm(pbes &p, data::rewrite_strategy rewrite_strategy, pbes_rewriter_type rewriter_type, bool compute_conditions = false, bool remove_redundant_equations = true, bool check_quantifiers = true)

Apply the constelm algorithm.

Parameters:

• p A PBES to which the algorithm is applied
• rewrite_strategy A data rewrite strategy
• rewriter_type A PBES rewriter type
• compute_conditions If true, conditions for the edges of the dependency graph are used N.B. Very inefficient!
• remove_redundant_equations If true, unreachable equations will be removed.

void pbesconstelm(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, data::rewrite_strategy rewrite_strategy, pbes_rewriter_type rewriter_type, bool compute_conditions, bool remove_redundant_equations, bool check_quantifiers)

Functions

void mcrl2::pbes_system::detail::make_constelm_substitution(const std::map<data::variable, data::data_expression> &m, data::rewriter::substitution_type &result)