Sequence Chart Studio  svn HEAD revision
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Public Member Functions | Private Member Functions | Private Attributes | List of all members
FootprintTraverser Class Reference

#include <race_checker.h>

Inheritance diagram for FootprintTraverser:
Inheritance graph
Collaboration diagram for FootprintTraverser:
Collaboration graph

Public Member Functions

 FootprintTraverser (HMsc *hmsc, ChannelMapper *mapper, size_t instances_count, MinimalEventsInitiator *min, MaximalEventsInitiator *max)
 
void on_white_node_found (ReferenceNode *node)
 
void on_gray_node_found (ReferenceNode *n)
 
void traverse ()
 
const std::list
< RaceInHMscException > & 
get_counterexamples ()
 
void traverse (HMscNode *node)
 
void cleanup ()
 
- Public Member Functions inherited from WhiteRefNodeFoundListener
virtual ~WhiteRefNodeFoundListener ()
 
virtual void on_white_node_found (HMscNode *n)
 
- Public Member Functions inherited from WhiteNodeFoundListener
virtual ~WhiteNodeFoundListener ()
 
- Public Member Functions inherited from NodeFinder
 NodeFinder (const std::string &color_attribute="rnf_color")
 
HMscNodePListPtr find_successors (HMscNode *node)
 Finds nearest (possibly indirect) successors of a node which satisfy the is_terminal() condition. More...
 
HMscNodePListPtr find_predecessors (HMscNode *node)
 Dual function to find_successors(). More...
 
virtual bool is_terminal (HMscNode *node)
 A predicate telling whether searching for successors should continue from the given node. It continues only if terminal(node) == false. More...
 
HMscNodePListPtr get_result (void)
 Returns the result of find_successors() or find_predecessors(). More...
 
HMscNodePListPtr get_skipped (void)
 Returns nodes skipped by find_successors() or find_predecessors(). Connection nodes are not stored. More...
 
void find_node (HMscNode *start, HMscNode *desired)
 Finds path from start to desired node. It always proceeds forward. More...
 
- Public Member Functions inherited from DFSBMscGraphTraverser
 DFSBMscGraphTraverser (const std::string &color_attribute="msc_graph_traverse_color")
 
virtual ~DFSBMscGraphTraverser ()
 
virtual void traverse (HMscPtr hmsc)
 
virtual void cleanup_traversing_attributes ()
 
const MscElementPListListget_reached_elements ()
 
- Public Member Functions inherited from DFSListenersContainer
void add_node_finished_listener (NodeFinishedListenerP l)
 
void remove_node_finished_listeners ()
 
void add_white_node_found_listener (WhiteNodeFoundListenerP l)
 
void remove_white_node_found_listeners ()
 
void add_gray_node_found_listener (GrayNodeFoundListenerP l)
 
void remove_gray_node_found_listeners ()
 
void add_black_node_found_listener (BlackNodeFoundListenerP l)
 
void remove_black_node_found_listeners ()
 
void remove_all_listeners ()
 
virtual ~DFSListenersContainer ()
 
- Public Member Functions inherited from GrayRefNodeFoundListener
virtual ~GrayRefNodeFoundListener ()
 
virtual void on_gray_node_found (HMscNode *n)
 
- Public Member Functions inherited from GrayNodeFoundListener
virtual ~GrayNodeFoundListener ()
 

Private Member Functions

FootprintPtr extract_todo ()
 
void check_race (BMsc *b, FootprintPtr &f)
 

Private Attributes

std::set< FootprintPtr,
FootprintPtrComparator
todo
 
std::set< FootprintPtr,
FootprintPtrComparator
done
 
std::list< RaceInHMscExceptionm_counterexamples
 
ChannelMapperm_mapper
 
MinimalEventsInitiatorm_min
 
MaximalEventsInitiatorm_max
 
FootprintPtr m_footprint
 
HMscNodem_first_node
 The node with the "first node" attribute set. It is necessary for cleanup. More...
 

Additional Inherited Members

- Static Public Member Functions inherited from NodeFinder
static HMscNodePListPtr successors (HMscNode *node, const std::string &color_attribute="rnf_color")
 Creates ReferenceNodeFinder and returns result of find_successors(). For derrived classes use the template version. More...
 
static HMscNodePListPtr predecessors (HMscNode *node, const std::string &color_attribute="rnf_color")
 Creates ReferenceNodeFinder and returns result of find_predecessors(). For derrived classes use the template version. More...
 
template<class T >
static HMscNodePListPtr successors (HMscNode *node, const std::string &color_attribute="rnf_color")
 Creates a finder of the type T and returns its result of find_successors(). More...
 
template<class T >
static HMscNodePListPtr predecessors (HMscNode *node, const std::string &color_attribute="rnf_color")
 Creates a finder of the type T and returns its result of find_predecessors(). More...
 
- Protected Member Functions inherited from NodeFinder
bool traverse_node (HMscNode *node)
 Traverses from node to nearest StartNode,EndNodes or ReferenceNodes. More...
 
void traverse_predecessors (SuccessorNode *succ)
 Traverses predecessors of a given node. More...
 
- Protected Member Functions inherited from DFSBMscGraphTraverser
virtual void cleanup_top_attributes ()
 
virtual bool traverse_successors (PredecessorNode *predecessor)
 
virtual bool is_processed (HMscNode *node)
 
virtual bool traverse_reference_node (ReferenceNode *node)
 
void set_color (HMscNode *n, NodeColor c)
 
NodeColorget_color (HMscNode *n)
 
virtual void push_top_attributes ()
 
virtual void white_node_found (HMscNode *n)
 
virtual void gray_node_found (HMscNode *n)
 
virtual void black_node_found (HMscNode *n)
 
virtual void node_finished (HMscNode *n)
 
- Protected Attributes inherited from NodeFinder
bool m_running_forward
 True when find_successors() is in progress, false if find_predecessors() works. More...
 
HMscNodePListPtr m_result
 Stores the result of find_successors() or find_predecessors() More...
 
HMscNodePListPtr m_skipped_nodes
 Stores nodes skipped by find_successors() or find_predecessors() More...
 
- Protected Attributes inherited from DFSBMscGraphTraverser
HMscNodePListList m_colored_nodes
 
MscElementPListList m_reached_elements
 
std::string m_color_attribute
 
- Protected Attributes inherited from DFSListenersContainer
NodeFinishedListenerPList m_node_finished_listeners
 
WhiteNodeFoundListenerPList m_white_node_found_listeners
 
GrayNodeFoundListenerPList m_gray_node_found_listeners
 
BlackNodeFoundListenerPList m_black_node_found_listeners
 
GrayNodeFoundListenerPList m_grey_node_found_listeners
 

Detailed Description

Definition at line 132 of file race_checker.h.

Constructor & Destructor Documentation

FootprintTraverser::FootprintTraverser ( HMsc hmsc,
ChannelMapper mapper,
size_t  instances_count,
MinimalEventsInitiator min,
MaximalEventsInitiator max 
)

Member Function Documentation

void FootprintTraverser::check_race ( BMsc b,
FootprintPtr f 
)
private
void FootprintTraverser::cleanup ( )
inline

Definition at line 185 of file race_checker.h.

References m_first_node, and MscElement::remove_attribute().

FootprintPtr FootprintTraverser::extract_todo ( )
private

Definition at line 543 of file race_checker.cpp.

References todo.

Referenced by traverse().

const std::list<RaceInHMscException>& FootprintTraverser::get_counterexamples ( )
inline

Definition at line 178 of file race_checker.h.

References m_counterexamples.

void FootprintTraverser::on_gray_node_found ( ReferenceNode n)
inlinevirtual
void FootprintTraverser::on_white_node_found ( ReferenceNode node)
virtual
void FootprintTraverser::traverse ( )
void FootprintTraverser::traverse ( HMscNode node)
virtual

Member Data Documentation

std::set<FootprintPtr,FootprintPtrComparator> FootprintTraverser::done
private

Definition at line 137 of file race_checker.h.

Referenced by on_white_node_found(), and traverse().

std::list<RaceInHMscException> FootprintTraverser::m_counterexamples
private

Definition at line 138 of file race_checker.h.

Referenced by check_race(), and get_counterexamples().

HMscNode* FootprintTraverser::m_first_node
private

The node with the "first node" attribute set. It is necessary for cleanup.

Definition at line 149 of file race_checker.h.

Referenced by cleanup(), and traverse().

FootprintPtr FootprintTraverser::m_footprint
private

Definition at line 144 of file race_checker.h.

Referenced by check_race(), on_white_node_found(), and traverse().

ChannelMapper* FootprintTraverser::m_mapper
private

Definition at line 140 of file race_checker.h.

Referenced by check_race(), and FootprintTraverser().

MaximalEventsInitiator* FootprintTraverser::m_max
private

Definition at line 142 of file race_checker.h.

Referenced by FootprintTraverser(), and on_white_node_found().

MinimalEventsInitiator* FootprintTraverser::m_min
private

Definition at line 141 of file race_checker.h.

Referenced by check_race(), and FootprintTraverser().

std::set<FootprintPtr,FootprintPtrComparator> FootprintTraverser::todo
private

Definition at line 136 of file race_checker.h.

Referenced by extract_todo(), FootprintTraverser(), on_white_node_found(), and traverse().


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

SourceForge.net Logo
Generated on Fri Jan 15 2016 16:26:58 for Sequence Chart Studio by  doxygen