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
mcrl2::pbes_system::propositional_variable_substitution::const_iterator¶ typedef for
map_type::const_iterator
-
type
mcrl2::pbes_system::propositional_variable_substitution::expression_type¶ typedef for
pbes_expressiontype used to represent expressions
-
type
mcrl2::pbes_system::propositional_variable_substitution::iterator¶ typedef for
map_type::iterator
-
type
mcrl2::pbes_system::propositional_variable_substitution::map_type¶ typedef for
std::map< core::identifier_string, std::pair< pbes_expression, data::variable_list > >
-
type
mcrl2::pbes_system::propositional_variable_substitution::variable_type¶ typedef for
propositional_variable_instantiationtype used to represent variables
Protected attributes¶
-
map_type
mcrl2::pbes_system::propositional_variable_substitution::m_map¶
Public member functions¶
-
iterator
begin() Returns an iterator pointing to the beginning of the sequence of assignments.
-
const_iterator
begin() const Returns an iterator pointing to the beginning of the sequence of assignments.
-
bool
empty() const Returns true if the sequence of assignments is empty.
-
iterator
end() Returns an iterator pointing past the end of the sequence of assignments.
-
const_iterator
end() const 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.
