mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor Class Reference

#include <liblts_bisim_gjkw.h>

Public Member Functions

 B_to_C_descriptor (B_to_C_iter_t begin_, B_to_C_iter_t end_)
 
const block_tfrom_block () const
 compute the source block of the transitions in this slice
 
block_tfrom_block ()
 
const constln_tto_constln () const
 compute the goal constellation of the transitions in this slice
 
constln_tto_constln ()
 
bool needs_postprocessing () const
 returns true iff the slice is marked for postprocessing
 
std::string debug_id () const
 print a B_to_C slice identification for debugging
 
bool add_work_to_bottom_transns (enum check_complexity::counter_type ctr, unsigned max_value)
 

Public Attributes

B_to_C_iter_t end
 
B_to_C_iter_t begin
 
check_complexity::B_to_C_counter_t work_counter
 

Detailed Description

Definition at line 1340 of file liblts_bisim_gjkw.h.


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