mcrl2/pbes/constelm.h

Include file:

#include "mcrl2/pbes/constelm.h"

The constelm algorithm.

Classes

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)