mcrl2::pbes_system::pbes_constelm_algorithm::edge

Include file:

#include "mcrl2/pbes/constelm.h

class mcrl2::pbes_system::pbes_constelm_algorithm::edge

Represents an edge of the dependency graph. The assignments are stored implicitly using the ‘right’ parameter. The condition determines under what circumstances the influence of the edge is propagated to its target vertex.

Protected attributes

const std::set<data::variable> mcrl2::pbes_system::pbes_constelm_algorithm::edge::m_conj_context

const std::set<data::variable> mcrl2::pbes_system::pbes_constelm_algorithm::edge::m_disj_context

const qvar_list mcrl2::pbes_system::pbes_constelm_algorithm::edge::m_qvars

The quantifiers in whose direct context the target PVI occurs.

const propositional_variable mcrl2::pbes_system::pbes_constelm_algorithm::edge::m_source

The propositional variable at the source of the edge.

const propositional_variable_instantiation mcrl2::pbes_system::pbes_constelm_algorithm::edge::m_target

The propositional variable instantiation that determines the target of the edge.

Public member functions

const data::data_expression &condition() const

The condition of the edge.

edge() = default

Constructor.

edge(const propositional_variable &src, const qvar_list &qvars, const propositional_variable_instantiation &tgt, const std::set<data::variable> &conj_context, const std::set<data::variable> &disj_context, data::data_expression c = data::sort_bool::true_())

Constructor.

Parameters:

• src A propositional variable declaration
• tgt A propositional variable
• c A term

const qvar_list &quantified_variables() const

qvar_list quantifier_inside_approximation(const qvar_list &Q) const

Try to guess which quantifiers of Q can end up directly before target, when the quantifier inside rewriter is applied.

const propositional_variable &source() const

The propositional variable at the source of the edge.

const propositional_variable_instantiation &target() const

The propositional variable instantiation that determines the target of the edge.

std::string to_string() const

Returns a string representation of the edge.

Returns: A string representation of the edge.