mCRL2
Loading...
Searching...
No Matches
mcrl2::process::alphabet_operations Namespace Reference

Classes

struct  rename_inverse_apply
 

Typedefs

typedef std::map< core::identifier_string, std::vector< core::identifier_string > > rename_inverse_map
 

Functions

bool subset_includes (const allow_set &A, const multi_action_name &alpha)
 
multi_action_name_set set_intersection (const allow_set &A1, const multi_action_name_set &A)
 
std::pair< multi_action_name_set, bool > bounded_concat (const multi_action_name_set &A1, const multi_action_name_set &A2, const allow_set &A)
 
std::pair< multi_action_name_set, bool > bounded_merge (const multi_action_name_set &A1, const multi_action_name_set &A2, const allow_set &A)
 
std::pair< multi_action_name_set, bool > bounded_left_merge (const multi_action_name_set &A1, const multi_action_name_set &A2, const allow_set &A)
 
std::pair< multi_action_name_set, bool > bounded_sync (const multi_action_name_set &A1, const multi_action_name_set &A2, const allow_set &A)
 
allow_set block (const core::identifier_string_list &B, const allow_set &x)
 
allow_set hide_inverse (const core::identifier_string_list &I, const allow_set &x)
 
allow_set allow (const action_name_multiset_list &V, const allow_set &x)
 
allow_set rename_inverse (const rename_expression_list &R, const allow_set &x)
 
allow_set comm_inverse (const communication_expression_list &C, const allow_set &x)
 
allow_set left_arrow (const allow_set &x, const multi_action_name_set &A)
 
allow_set subsets (const allow_set &x)
 
bool includes (const multi_action_name &x, const multi_action_name &y)
 
bool contains (const multi_action_name &alpha, const core::identifier_string &a)
 
multi_action_name multiset_difference (const multi_action_name &alpha, const multi_action_name &beta)
 
multi_action_name multiset_union (const multi_action_name &alpha, const multi_action_name &beta)
 
multi_action_name_set make_name_set (const action_name_multiset_list &v)
 
bool contains (const multi_action_name_set &A, const multi_action_name &a)
 
bool includes (const multi_action_name_set &A, const multi_action_name &y)
 
bool subset_includes (const multi_action_name_set &A, const multi_action_name &x)
 
multi_action_name_set set_difference (const multi_action_name_set &A1, const multi_action_name_set &A2)
 
multi_action_name_set set_union (const multi_action_name_set &A1, const multi_action_name_set &A2)
 
multi_action_name_set set_intersection (const multi_action_name_set &A1, const multi_action_name_set &A2)
 
multi_action_name_set remove_subsets (const multi_action_name_set &A)
 
multi_action_name_set block (const core::identifier_string_list &B, const multi_action_name_set &A, bool A_includes_subsets=false)
 
multi_action_name hide (const multi_action_name &alpha, const std::set< core::identifier_string > &I)
 
std::set< core::identifier_stringhide (const core::identifier_string_list &I, const std::set< core::identifier_string > &J)
 
multi_action_name hide (const std::set< core::identifier_string > &I, const multi_action_name &alpha)
 
template<typename IdentifierContainer >
multi_action_name_set hide (const IdentifierContainer &I, const multi_action_name_set &A, bool=false)
 
multi_action_name_set hide_inverse (const core::identifier_string_list &I, const multi_action_name_set &A, bool A_includes_subsets=false)
 
multi_action_name_set concat (const multi_action_name_set &A1, const multi_action_name_set &A2)
 
bool concat_includes (const multi_action_name_set &A1, const multi_action_name_set &A2, const multi_action_name &alpha)
 
multi_action_name_set bounded_concat (const multi_action_name_set &A1, const multi_action_name_set &A2, const multi_action_name_set &A)
 
multi_action_name_set left_arrow1 (const multi_action_name_set &A1, const multi_action_name_set &A2)
 
multi_action_name_set left_arrow (const multi_action_name_set &A1, bool A1_includes_subsets, const multi_action_name_set &A2)
 
multi_action_name_set left_arrow2 (const multi_action_name_set &A, const std::set< core::identifier_string > &I, const multi_action_name_set &A2)
 
multi_action_name_set merge (const multi_action_name_set &A1, const multi_action_name_set &A2)
 
multi_action_name_set bounded_merge (const multi_action_name_set &A1, const multi_action_name_set &A2, const multi_action_name_set &A)
 
multi_action_name_set left_merge (const multi_action_name_set &A1, const multi_action_name_set &A2)
 
multi_action_name_set sync (const multi_action_name_set &A1, const multi_action_name_set &A2)
 
multi_action_name_set bounded_sync (const multi_action_name_set &A1, const multi_action_name_set &A2, const multi_action_name_set &A)
 
std::pair< multi_action_name, multi_action_nameapply_comm_inverse (const communication_expression &x, const multi_action_name &alpha1, const multi_action_name &alpha2)
 
void apply_comm_inverse (const communication_expression &gamma, multi_action_name_set &A)
 
void comm_inverse (const communication_expression_list &C, const multi_action_name &alpha1, const multi_action_name &alpha2, multi_action_name_set &result)
 
multi_action_name_set comm_inverse1 (const communication_expression_list &C, const multi_action_name_set &A)
 
multi_action_name_set comm_inverse (const communication_expression_list &C, const multi_action_name_set &A, bool=false)
 
std::set< core::identifier_stringcomm_inverse (const communication_expression_list &C, const std::set< core::identifier_string > &I)
 
void apply_comm (const communication_expression &c, multi_action_name_set &A)
 
multi_action_name_set comm (const communication_expression_list &C, const multi_action_name_set &A, bool=false)
 
communication_expression_list filter_comm_set (const communication_expression_list &C, const multi_action_name_set &alphabet)
 
bool is_source (const rename_expression_list &R, const core::identifier_string &x)
 
core::identifier_string apply_rename (const rename_expression_list &R, const core::identifier_string &x)
 
multi_action_name apply_rename (const rename_expression_list &R, const multi_action_name &a)
 
multi_action_name_set rename (const rename_expression_list &R, const multi_action_name_set &A, bool=false)
 Computes R(A)
 
rename_inverse_map rename_inverse (const rename_expression_list &R)
 
std::string print_rename_inverse_map (const rename_inverse_map &m)
 
std::set< core::identifier_stringrename_inverse (const rename_expression_list &R, const std::set< core::identifier_string > &I)
 
void rename_inverse (const rename_inverse_map &Rinverse, const multi_action_name &x, bool x_includes_subsets, multi_action_name_set &result)
 
multi_action_name_set rename_inverse (const rename_expression_list &R, const multi_action_name_set &A, bool A_includes_subsets=false)
 Computes R^[-1}(A)
 
multi_action_name_set allow (const action_name_multiset_list &V, const multi_action_name_set &A, bool A_includes_subsets=false)
 

Typedef Documentation

◆ rename_inverse_map

Function Documentation

◆ allow() [1/2]

allow_set mcrl2::process::alphabet_operations::allow ( const action_name_multiset_list V,
const allow_set x 
)
inline

Definition at line 273 of file allow_set.h.

◆ allow() [2/2]

multi_action_name_set mcrl2::process::alphabet_operations::allow ( const action_name_multiset_list V,
const multi_action_name_set A,
bool  A_includes_subsets = false 
)
inline

Definition at line 760 of file alphabet_operations.h.

◆ apply_comm()

void mcrl2::process::alphabet_operations::apply_comm ( const communication_expression c,
multi_action_name_set A 
)
inline

Definition at line 517 of file alphabet_operations.h.

◆ apply_comm_inverse() [1/2]

void mcrl2::process::alphabet_operations::apply_comm_inverse ( const communication_expression gamma,
multi_action_name_set A 
)
inline

Definition at line 436 of file alphabet_operations.h.

◆ apply_comm_inverse() [2/2]

std::pair< multi_action_name, multi_action_name > mcrl2::process::alphabet_operations::apply_comm_inverse ( const communication_expression x,
const multi_action_name alpha1,
const multi_action_name alpha2 
)
inline

Definition at line 422 of file alphabet_operations.h.

◆ apply_rename() [1/2]

core::identifier_string mcrl2::process::alphabet_operations::apply_rename ( const rename_expression_list R,
const core::identifier_string x 
)
inline

Definition at line 589 of file alphabet_operations.h.

◆ apply_rename() [2/2]

multi_action_name mcrl2::process::alphabet_operations::apply_rename ( const rename_expression_list R,
const multi_action_name a 
)
inline

Definition at line 602 of file alphabet_operations.h.

◆ block() [1/2]

allow_set mcrl2::process::alphabet_operations::block ( const core::identifier_string_list B,
const allow_set x 
)
inline

Definition at line 250 of file allow_set.h.

◆ block() [2/2]

multi_action_name_set mcrl2::process::alphabet_operations::block ( const core::identifier_string_list B,
const multi_action_name_set A,
bool  A_includes_subsets = false 
)
inline

Definition at line 166 of file alphabet_operations.h.

◆ bounded_concat() [1/2]

std::pair< multi_action_name_set, bool > mcrl2::process::alphabet_operations::bounded_concat ( const multi_action_name_set A1,
const multi_action_name_set A2,
const allow_set A 
)
inline

Definition at line 205 of file allow_set.h.

◆ bounded_concat() [2/2]

multi_action_name_set mcrl2::process::alphabet_operations::bounded_concat ( const multi_action_name_set A1,
const multi_action_name_set A2,
const multi_action_name_set A 
)
inline

Definition at line 309 of file alphabet_operations.h.

◆ bounded_left_merge()

std::pair< multi_action_name_set, bool > mcrl2::process::alphabet_operations::bounded_left_merge ( const multi_action_name_set A1,
const multi_action_name_set A2,
const allow_set A 
)
inline

Definition at line 237 of file allow_set.h.

◆ bounded_merge() [1/2]

std::pair< multi_action_name_set, bool > mcrl2::process::alphabet_operations::bounded_merge ( const multi_action_name_set A1,
const multi_action_name_set A2,
const allow_set A 
)
inline

Definition at line 229 of file allow_set.h.

◆ bounded_merge() [2/2]

multi_action_name_set mcrl2::process::alphabet_operations::bounded_merge ( const multi_action_name_set A1,
const multi_action_name_set A2,
const multi_action_name_set A 
)
inline

Definition at line 393 of file alphabet_operations.h.

◆ bounded_sync() [1/2]

std::pair< multi_action_name_set, bool > mcrl2::process::alphabet_operations::bounded_sync ( const multi_action_name_set A1,
const multi_action_name_set A2,
const allow_set A 
)
inline

Definition at line 244 of file allow_set.h.

◆ bounded_sync() [2/2]

multi_action_name_set mcrl2::process::alphabet_operations::bounded_sync ( const multi_action_name_set A1,
const multi_action_name_set A2,
const multi_action_name_set A 
)
inline

Definition at line 412 of file alphabet_operations.h.

◆ comm()

multi_action_name_set mcrl2::process::alphabet_operations::comm ( const communication_expression_list C,
const multi_action_name_set A,
bool  = false 
)
inline

Definition at line 541 of file alphabet_operations.h.

◆ comm_inverse() [1/4]

allow_set mcrl2::process::alphabet_operations::comm_inverse ( const communication_expression_list C,
const allow_set x 
)
inline

Definition at line 298 of file allow_set.h.

◆ comm_inverse() [2/4]

void mcrl2::process::alphabet_operations::comm_inverse ( const communication_expression_list C,
const multi_action_name alpha1,
const multi_action_name alpha2,
multi_action_name_set result 
)
inline

Definition at line 460 of file alphabet_operations.h.

◆ comm_inverse() [3/4]

multi_action_name_set mcrl2::process::alphabet_operations::comm_inverse ( const communication_expression_list C,
const multi_action_name_set A,
bool  = false 
)
inline

Definition at line 487 of file alphabet_operations.h.

◆ comm_inverse() [4/4]

std::set< core::identifier_string > mcrl2::process::alphabet_operations::comm_inverse ( const communication_expression_list C,
const std::set< core::identifier_string > &  I 
)
inline

Definition at line 499 of file alphabet_operations.h.

◆ comm_inverse1()

multi_action_name_set mcrl2::process::alphabet_operations::comm_inverse1 ( const communication_expression_list C,
const multi_action_name_set A 
)
inline

Definition at line 475 of file alphabet_operations.h.

◆ concat()

multi_action_name_set mcrl2::process::alphabet_operations::concat ( const multi_action_name_set A1,
const multi_action_name_set A2 
)
inline

Definition at line 276 of file alphabet_operations.h.

◆ concat_includes()

bool mcrl2::process::alphabet_operations::concat_includes ( const multi_action_name_set A1,
const multi_action_name_set A2,
const multi_action_name alpha 
)
inline

Definition at line 292 of file alphabet_operations.h.

◆ contains() [1/2]

bool mcrl2::process::alphabet_operations::contains ( const multi_action_name alpha,
const core::identifier_string a 
)
inline

Definition at line 38 of file alphabet_operations.h.

◆ contains() [2/2]

bool mcrl2::process::alphabet_operations::contains ( const multi_action_name_set A,
const multi_action_name a 
)
inline

Definition at line 84 of file alphabet_operations.h.

◆ filter_comm_set()

communication_expression_list mcrl2::process::alphabet_operations::filter_comm_set ( const communication_expression_list C,
const multi_action_name_set alphabet 
)
inline

Definition at line 555 of file alphabet_operations.h.

◆ hide() [1/4]

std::set< core::identifier_string > mcrl2::process::alphabet_operations::hide ( const core::identifier_string_list I,
const std::set< core::identifier_string > &  J 
)
inline

Definition at line 220 of file alphabet_operations.h.

◆ hide() [2/4]

template<typename IdentifierContainer >
multi_action_name_set mcrl2::process::alphabet_operations::hide ( const IdentifierContainer &  I,
const multi_action_name_set A,
bool  = false 
)

Definition at line 250 of file alphabet_operations.h.

◆ hide() [3/4]

multi_action_name mcrl2::process::alphabet_operations::hide ( const multi_action_name alpha,
const std::set< core::identifier_string > &  I 
)
inline

Definition at line 204 of file alphabet_operations.h.

◆ hide() [4/4]

multi_action_name mcrl2::process::alphabet_operations::hide ( const std::set< core::identifier_string > &  I,
const multi_action_name alpha 
)
inline

Definition at line 235 of file alphabet_operations.h.

◆ hide_inverse() [1/2]

allow_set mcrl2::process::alphabet_operations::hide_inverse ( const core::identifier_string_list I,
const allow_set x 
)
inline

Definition at line 263 of file allow_set.h.

◆ hide_inverse() [2/2]

multi_action_name_set mcrl2::process::alphabet_operations::hide_inverse ( const core::identifier_string_list I,
const multi_action_name_set A,
bool  A_includes_subsets = false 
)
inline

Definition at line 266 of file alphabet_operations.h.

◆ includes() [1/2]

bool mcrl2::process::alphabet_operations::includes ( const multi_action_name x,
const multi_action_name y 
)
inline

Definition at line 32 of file alphabet_operations.h.

◆ includes() [2/2]

bool mcrl2::process::alphabet_operations::includes ( const multi_action_name_set A,
const multi_action_name y 
)
inline

Definition at line 92 of file alphabet_operations.h.

◆ is_source()

bool mcrl2::process::alphabet_operations::is_source ( const rename_expression_list R,
const core::identifier_string x 
)
inline

Definition at line 576 of file alphabet_operations.h.

◆ left_arrow() [1/2]

allow_set mcrl2::process::alphabet_operations::left_arrow ( const allow_set x,
const multi_action_name_set A 
)
inline

Definition at line 306 of file allow_set.h.

◆ left_arrow() [2/2]

multi_action_name_set mcrl2::process::alphabet_operations::left_arrow ( const multi_action_name_set A1,
bool  A1_includes_subsets,
const multi_action_name_set A2 
)
inline

Definition at line 348 of file alphabet_operations.h.

◆ left_arrow1()

multi_action_name_set mcrl2::process::alphabet_operations::left_arrow1 ( const multi_action_name_set A1,
const multi_action_name_set A2 
)
inline

Definition at line 327 of file alphabet_operations.h.

◆ left_arrow2()

multi_action_name_set mcrl2::process::alphabet_operations::left_arrow2 ( const multi_action_name_set A,
const std::set< core::identifier_string > &  I,
const multi_action_name_set A2 
)
inline

Definition at line 364 of file alphabet_operations.h.

◆ left_merge()

multi_action_name_set mcrl2::process::alphabet_operations::left_merge ( const multi_action_name_set A1,
const multi_action_name_set A2 
)
inline

Definition at line 399 of file alphabet_operations.h.

◆ make_name_set()

multi_action_name_set mcrl2::process::alphabet_operations::make_name_set ( const action_name_multiset_list v)
inline

Definition at line 72 of file alphabet_operations.h.

◆ merge()

multi_action_name_set mcrl2::process::alphabet_operations::merge ( const multi_action_name_set A1,
const multi_action_name_set A2 
)
inline

Definition at line 386 of file alphabet_operations.h.

◆ multiset_difference()

multi_action_name mcrl2::process::alphabet_operations::multiset_difference ( const multi_action_name alpha,
const multi_action_name beta 
)
inline

Definition at line 45 of file alphabet_operations.h.

◆ multiset_union()

multi_action_name mcrl2::process::alphabet_operations::multiset_union ( const multi_action_name alpha,
const multi_action_name beta 
)
inline

Definition at line 60 of file alphabet_operations.h.

◆ print_rename_inverse_map()

std::string mcrl2::process::alphabet_operations::print_rename_inverse_map ( const rename_inverse_map m)
inline

Definition at line 644 of file alphabet_operations.h.

◆ remove_subsets()

multi_action_name_set mcrl2::process::alphabet_operations::remove_subsets ( const multi_action_name_set A)
inline

Definition at line 148 of file alphabet_operations.h.

◆ rename()

multi_action_name_set mcrl2::process::alphabet_operations::rename ( const rename_expression_list R,
const multi_action_name_set A,
bool  = false 
)
inline

Computes R(A)

Definition at line 614 of file alphabet_operations.h.

◆ rename_inverse() [1/5]

rename_inverse_map mcrl2::process::alphabet_operations::rename_inverse ( const rename_expression_list R)
inline

Definition at line 628 of file alphabet_operations.h.

◆ rename_inverse() [2/5]

allow_set mcrl2::process::alphabet_operations::rename_inverse ( const rename_expression_list R,
const allow_set x 
)
inline

Definition at line 290 of file allow_set.h.

◆ rename_inverse() [3/5]

multi_action_name_set mcrl2::process::alphabet_operations::rename_inverse ( const rename_expression_list R,
const multi_action_name_set A,
bool  A_includes_subsets = false 
)
inline

Computes R^[-1}(A)

Definition at line 743 of file alphabet_operations.h.

◆ rename_inverse() [4/5]

std::set< core::identifier_string > mcrl2::process::alphabet_operations::rename_inverse ( const rename_expression_list R,
const std::set< core::identifier_string > &  I 
)
inline

Definition at line 689 of file alphabet_operations.h.

◆ rename_inverse() [5/5]

void mcrl2::process::alphabet_operations::rename_inverse ( const rename_inverse_map Rinverse,
const multi_action_name x,
bool  x_includes_subsets,
multi_action_name_set result 
)
inline

Definition at line 710 of file alphabet_operations.h.

◆ set_difference()

multi_action_name_set mcrl2::process::alphabet_operations::set_difference ( const multi_action_name_set A1,
const multi_action_name_set A2 
)
inline

Definition at line 123 of file alphabet_operations.h.

◆ set_intersection() [1/2]

multi_action_name_set mcrl2::process::alphabet_operations::set_intersection ( const allow_set A1,
const multi_action_name_set A 
)
inline

Definition at line 190 of file allow_set.h.

◆ set_intersection() [2/2]

multi_action_name_set mcrl2::process::alphabet_operations::set_intersection ( const multi_action_name_set A1,
const multi_action_name_set A2 
)
inline

Definition at line 139 of file alphabet_operations.h.

◆ set_union()

multi_action_name_set mcrl2::process::alphabet_operations::set_union ( const multi_action_name_set A1,
const multi_action_name_set A2 
)
inline

Definition at line 131 of file alphabet_operations.h.

◆ subset_includes() [1/2]

bool mcrl2::process::alphabet_operations::subset_includes ( const allow_set A,
const multi_action_name alpha 
)
inline

Definition at line 175 of file allow_set.h.

◆ subset_includes() [2/2]

bool mcrl2::process::alphabet_operations::subset_includes ( const multi_action_name_set A,
const multi_action_name x 
)
inline

Definition at line 110 of file alphabet_operations.h.

◆ subsets()

allow_set mcrl2::process::alphabet_operations::subsets ( const allow_set x)
inline

Definition at line 319 of file allow_set.h.

◆ sync()

multi_action_name_set mcrl2::process::alphabet_operations::sync ( const multi_action_name_set A1,
const multi_action_name_set A2 
)
inline

Definition at line 405 of file alphabet_operations.h.