Include file:

#include "mcrl2/pbes/eqelm.h
class mcrl2::pbes_system::pbes_eqelm_algorithm

Algorithm class for the eqelm algorithm.

Protected types

type mcrl2::pbes_system::pbes_eqelm_algorithm::equivalence_class

typedef for std::set< data::variable >

Protected attributes

const DataRewriter &mcrl2::pbes_system::pbes_eqelm_algorithm::m_data_rewriter

Compares data expressions for equality.

std::map<core::identifier_string, bool> mcrl2::pbes_system::pbes_eqelm_algorithm::m_discovered

Used for determining if a vertex has been visited before.

std::map<core::identifier_string, std::set<propositional_variable_instantiation>> mcrl2::pbes_system::pbes_eqelm_algorithm::m_edges

The edges of the graph. It is a mapping from X to iocc(X).

std::map<core::identifier_string, std::vector<data::variable>> mcrl2::pbes_system::pbes_eqelm_algorithm::m_parameters

The parameters of the propositional variable declarations. These are stored inside a vector, for efficiency reasons.

const PbesRewriter &mcrl2::pbes_system::pbes_eqelm_algorithm::m_pbes_rewriter

Compares data expressions for equality.

std::map<core::identifier_string, std::vector<equivalence_class>> mcrl2::pbes_system::pbes_eqelm_algorithm::m_vertices

The vertices of the grapth, i.e. the equivalence relations. It stores the equivalence sets for each propositional variable, for example X -> [ {x1, x3}, {x2, x4} ]. Equivalence sets of size 1 are not stored.

Protected member functions

void apply_equivalence_relations(pbes &p)

Chooses one parameter for every equivalence class, and removes the others. All occurrences of the removed parameters are replaced by the chosen parameter.

std::vector<equivalence_class> compute_equivalence_sets(const propositional_variable &X) const

Puts all parameters of the same sort in the same equivalence set.

data::mutable_map_substitution compute_substitution(const core::identifier_string &X)

Computes a substitution that corresponds to the equivalence relations in X.

bool evaluate_guard(const core::identifier_string&, const propositional_variable_instantiation&)

Returns true if the vertex X should propagate its values to Y.

std::size_t index_of(const data::variable &x, const VariableContainer &v)

Returns the index of the element x in the sequence v.

void log_todo_list(const std::set<core::identifier_string> &todo, const std::string &msg = "") const

Prints the todo list.

std::string print_edges() const

Prints the edges of the dependency graph.

std::string print_equivalence_classes() const

Prints the equivalence classes.

std::string print_vertices() const

Prints the vertices of the dependency graph.

void update_equivalence_classes(const propositional_variable_instantiation &Ye, const Substitution &vX, std::set<core::identifier_string> &todo)

Propagate the equivalence relations given by the substitution vX over the edge Ye.

Public member functions

pbes_eqelm_algorithm(const DataRewriter &datar, const PbesRewriter &pbesr)



  • datar A data rewriter
  • pbesr A PBES rewriter
void run(pbes &p, bool ignore_initial_state = false)

Runs the eqelm algorithm.


  • p A pbes
  • ignore_initial_state If true, the initial state is ignored.