mcrl2::pbes_system::pbes_constelm_algorithm

Include file:

#include "mcrl2/pbes/constelm.h

class mcrl2::pbes_system::pbes_constelm_algorithm

Algorithm class for the constelm algorithm.

Protected types

type mcrl2::pbes_system::pbes_constelm_algorithm::constraint_map

typedef for std::map< data::variable, data::data_expression >

A map with constraints on the vertices of the graph.

type mcrl2::pbes_system::pbes_constelm_algorithm::edge_map

typedef for std::map< core::identifier_string, std::vector< edge > >

The storage type for edges.

type mcrl2::pbes_system::pbes_constelm_algorithm::qvar_list

typedef for std::list< detail::quantified_variable >

type mcrl2::pbes_system::pbes_constelm_algorithm::vertex_map

typedef for std::map< core::identifier_string, vertex >

The storage type for vertices.

Protected attributes

const DataRewriter &mcrl2::pbes_system::pbes_constelm_algorithm::m_data_rewriter

Compares data expressions for equality.

edge_map mcrl2::pbes_system::pbes_constelm_algorithm::m_edges

The edges of the dependency graph. They are stored in a map, to easily access all out-edges corresponding to a particular vertex.

const PbesRewriter &mcrl2::pbes_system::pbes_constelm_algorithm::m_pbes_rewriter

Compares data expressions for equality.

std::map<core::identifier_string, std::vector<std::size_t>> mcrl2::pbes_system::pbes_constelm_algorithm::m_redundant_parameters

The redundant parameters.

vertex_map mcrl2::pbes_system::pbes_constelm_algorithm::m_vertices

The vertices of the dependency graph. They are stored in a map, to support searching for a vertex.

Protected member functions

std::list<E> concat(const std::list<E> a, const std::list<E> b)

std::string print_condition(const edge &e, const vertex &u, const pbes_expression &value)

std::string print_edge_update(const edge &e, const vertex &u, const vertex &v)

std::string print_edges()

Logs the edges of the dependency graph.

std::string print_evaluation_failure(const edge &e, const vertex &u)

std::string print_todo_list(const std::deque<propositional_variable> &todo)

std::string print_vertices() const

Logs the vertices of the dependency graph.

Public member functions

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

Constructor.

Parameters:

• datar A data rewriter
• pbesr A PBES rewriter

std::map<propositional_variable, std::vector<data::variable>> redundant_parameters() const

Returns the parameters that have been removed by the constelm algorithm.

Returns: The removed parameters

void run(pbes &p, bool compute_conditions = false, bool check_quantifiers = true)

Runs the constelm algorithm.

Parameters:

• p A pbes
• compute_conditions If true, propagation conditions are computed. Note that the currently implementation has exponential behavior.