mcrl2::pbes_system::detail::rewrite_star_substitution Struct Reference

#include <pbesinst_lazy_counter_example.h>

Public Member Functions
	rewrite_star_substitution (const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const structure_graph &G, bool alpha, const std::unordered_map< pbes_expression, structure_graph::index_type > &mapping, const std::unordered_map< std::string, std::set< int > > &R)
pbes_expression	operator() (const propositional_variable_instantiation &Y) const

Public Attributes
const fixpoint_symbol &	symbol
const propositional_variable_instantiation &	X
const structure_graph &	G
bool	alpha
const std::unordered_map< pbes_expression, structure_graph::index_type > &	mapping
const std::unordered_map< std::string, std::set< int > > &	R

Detailed Description

Definition at line 62 of file pbesinst_lazy_counter_example.h.

Constructor & Destructor Documentation

rewrite_star_substitution()

mcrl2::pbes_system::detail::rewrite_star_substitution::rewrite_star_substitution ( const fixpoint_symbol &  symbol, const propositional_variable_instantiation &  X, const structure_graph &  G, bool  alpha, const std::unordered_map< pbes_expression, structure_graph::index_type > &  mapping, const std::unordered_map< std::string, std::set< int > > &  R  )

inline

Definition at line 71 of file pbesinst_lazy_counter_example.h.

Member Function Documentation

operator()()

pbes_expression mcrl2::pbes_system::detail::rewrite_star_substitution::operator() ( const propositional_variable_instantiation &  Y ) const

inline

Definition at line 85 of file pbesinst_lazy_counter_example.h.

Member Data Documentation

alpha

bool mcrl2::pbes_system::detail::rewrite_star_substitution::alpha

Definition at line 67 of file pbesinst_lazy_counter_example.h.

G

const structure_graph& mcrl2::pbes_system::detail::rewrite_star_substitution::G

Definition at line 66 of file pbesinst_lazy_counter_example.h.

mapping

const std::unordered_map<pbes_expression, structure_graph::index_type>& mcrl2::pbes_system::detail::rewrite_star_substitution::mapping

Definition at line 68 of file pbesinst_lazy_counter_example.h.

R

const std::unordered_map<std::string, std::set<int> >& mcrl2::pbes_system::detail::rewrite_star_substitution::R

Definition at line 69 of file pbesinst_lazy_counter_example.h.

symbol

const fixpoint_symbol& mcrl2::pbes_system::detail::rewrite_star_substitution::symbol

Definition at line 64 of file pbesinst_lazy_counter_example.h.

X

const propositional_variable_instantiation& mcrl2::pbes_system::detail::rewrite_star_substitution::X

Definition at line 65 of file pbesinst_lazy_counter_example.h.

---

The documentation for this struct was generated from the following file:

• pbes/include/mcrl2/pbes/pbesinst_lazy_counter_example.h