mcrl2::pbes_system::pbes_eqelm_algorithm¶
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.
