mcrl2::pbes_system::propositional_variable_substitution

Include file:

#include "mcrl2/pbes/substitutions.h
class mcrl2::pbes_system::propositional_variable_substitution

Substitution function for propositional variables.

Model of Substitution.

Public types

type const_iterator

typedef for map_type::const_iterator

type expression_type

typedef for pbes_expression

type used to represent expressions

type iterator

typedef for map_type::iterator

type map_type

typedef for std::map< core::identifier_string, std::pair< pbes_expression, data::variable_list > >

type variable_type

typedef for propositional_variable_instantiation

type used to represent variables

Protected attributes

map_type m_map

Public member functions

const_iterator begin() const

Returns an iterator pointing to the beginning of the sequence of assignments.

iterator begin()

Returns an iterator pointing to the beginning of the sequence of assignments.

bool empty() const

Returns true if the sequence of assignments is empty.

const_iterator end() const

Returns an iterator pointing past the end of the sequence of assignments.

iterator end()

Returns an iterator pointing past the end of the sequence of assignments.

map_type::size_type erase(const propositional_variable &v)

Removes the substitution to the propositional variable v.

iterator find(const variable_type &v)

Returns an iterator that references the expression associated with v or is equal to m_map.end()

const_iterator find(variable_type const &v) const

Returns an iterator that references the expression associated with v or is equal to m_map.end()

pbes_expression operator()(const variable_type &v) const

Apply this substitution to a single variable expression.

Parameters:

  • v The variable for which to give the associated expression.

Returns: expression equivalent to s(e), or a reference to such an expression.

assignment operator[](const propositional_variable &v)

Update substitution for a single variable.

Parameters:

  • v the variable for which to update the value

template<typenameE,typenameV>voidexample(Vconst&v,Econst&e){substitution<E,V>s;//substitutionstd::cout<<s(x)<<std::endl;//printsxs[v]=e;std::cout<<s(x)<<std::endl;//printse}

Returns: expression assignment for variable v, effect
propositional_variable_substitution() = default
propositional_variable_substitution(const map_type &other)
propositional_variable_substitution(const propositional_variable &X, const pbes_expression &phi)

Constructor. Initializes the substitution with the assignment X := phi.