mCRL2
Loading...
Searching...
No Matches
Public Member Functions | Protected Member Functions | Static Protected Member Functions | Protected Attributes | List of all members
mcrl2::lps::detail::comm_entry Class Reference

Data structure to store the communication function more efficiently. More...

#include <linearise_communication.h>

Public Member Functions

 comm_entry (const comm_entry &)=delete
 
comm_entry & operator= (const comm_entry &)=delete
 
 comm_entry (const process::communication_expression_list &communications)
 
 ~comm_entry ()=default
 
std::size_t size () const
 
process::action_label can_communicate (const process::action_list &m)
 
bool might_communicate (const process::action_list &m, const process::action_list &n)
 

Protected Member Functions

void reset_temporary_data ()
 
bool match_multiaction (const process::action_list &multi_action)
 

Static Protected Member Functions

static std::vector< core::identifier_string_list > init_lhs (const process::communication_expression_list &communications)
 
static std::vector< core::identifier_string > init_rhs (const process::communication_expression_list &communications)
 

Protected Attributes

const std::vector< core::identifier_string_list > m_lhs
 Left-hand sides of communication expressions.
 
const std::vector< core::identifier_string > m_rhs
 Right-hand sides of communication expressions.
 
std::vector< core::identifier_string_list::const_iterator > m_lhs_iters
 
std::vector< bool > m_match_failed
 

Detailed Description

Data structure to store the communication function more efficiently.

Definition at line 122 of file linearise_communication.h.

Constructor & Destructor Documentation

◆ comm_entry() [1/2]

mcrl2::lps::detail::comm_entry::comm_entry ( const comm_entry &  )
delete

◆ comm_entry() [2/2]

mcrl2::lps::detail::comm_entry::comm_entry ( const process::communication_expression_list &  communications)
inlineexplicit

Definition at line 226 of file linearise_communication.h.

◆ ~comm_entry()

mcrl2::lps::detail::comm_entry::~comm_entry ( )
default

Member Function Documentation

◆ can_communicate()

process::action_label mcrl2::lps::detail::comm_entry::can_communicate ( const process::action_list &  m)
inline

Determine if there exists a communication expression a1|...|an -> b in comm_table such that m' = a1|...|an , where m' is the multiset of actionnames for multiaction m. That is, the actions in m consting of actions and data occur in C, such tat a communication can take place.

if $\exists_{(b,c) \in C} b = \mu(m)$, return $c$, otherwise return action_label()

Definition at line 249 of file linearise_communication.h.

◆ init_lhs()

static std::vector< core::identifier_string_list > mcrl2::lps::detail::comm_entry::init_lhs ( const process::communication_expression_list &  communications)
inlinestaticprotected

Definition at line 196 of file linearise_communication.h.

◆ init_rhs()

static std::vector< core::identifier_string > mcrl2::lps::detail::comm_entry::init_rhs ( const process::communication_expression_list &  communications)
inlinestaticprotected

Definition at line 211 of file linearise_communication.h.

◆ match_multiaction()

bool mcrl2::lps::detail::comm_entry::match_multiaction ( const process::action_list &  multi_action)
inlineprotected

Check if m is contained in a lhs in the communication entry. (in fact, it must be a prefix). Returns true if this is the case, false otherwise. Postcondition: for every i such that m is not contained in lhs[i], match_failed[i] is true. NB: resets temporary data before performing computations.

Definition at line 149 of file linearise_communication.h.

◆ might_communicate()

bool mcrl2::lps::detail::comm_entry::might_communicate ( const process::action_list &  m,
const process::action_list &  n 
)
inline

Calculate $\exists_{o,c}\ (\mu(m) \oplus o,\ c) \in C$, with $o \subseteq n$

The function calculates whether the actions in m (consisting of actions and data) occur in a left hand side of a communication a1|...|ak -> b in C (that is, the names of m are a subbag of a1|...|ak), and the actions a1|...|ak that are not in m are in n. I.e., there is a subbag o of n such that m+o can communicate.

Definition at line 282 of file linearise_communication.h.

◆ operator=()

comm_entry & mcrl2::lps::detail::comm_entry::operator= ( const comm_entry &  )
delete

◆ reset_temporary_data()

void mcrl2::lps::detail::comm_entry::reset_temporary_data ( )
inlineprotected

Definition at line 136 of file linearise_communication.h.

◆ size()

std::size_t mcrl2::lps::detail::comm_entry::size ( ) const
inline

Definition at line 235 of file linearise_communication.h.

Member Data Documentation

◆ m_lhs

const std::vector<core::identifier_string_list> mcrl2::lps::detail::comm_entry::m_lhs
protected

Left-hand sides of communication expressions.

Definition at line 126 of file linearise_communication.h.

◆ m_lhs_iters

std::vector<core::identifier_string_list::const_iterator> mcrl2::lps::detail::comm_entry::m_lhs_iters
protected

Temporary data using in determining whether communication is allowed. See usages of the data structure below.

Definition at line 133 of file linearise_communication.h.

◆ m_match_failed

std::vector<bool> mcrl2::lps::detail::comm_entry::m_match_failed
protected

Definition at line 134 of file linearise_communication.h.

◆ m_rhs

const std::vector<core::identifier_string> mcrl2::lps::detail::comm_entry::m_rhs
protected

Right-hand sides of communication expressions.

Definition at line 129 of file linearise_communication.h.

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