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

#include <livelock_checker.h>

Inheritance diagram for LivelockChecker:
Inheritance graph
Collaboration diagram for LivelockChecker:
Collaboration graph

Public Member Functions

 LivelockChecker ()
virtual std::wstring get_property_name () const
virtual std::wstring get_help_filename () const
virtual PreconditionList get_preconditions (MscPtr msc) const
 Returns a list of preconditions for the check. More...
bool is_supported (ChannelMapperPtr chm)
 ~LivelockChecker ()
std::list< HMscPtrcheck (HMscPtr h, ChannelMapperPtr chm)
void cleanup_attributes ()
- Public Member Functions inherited from Checker
virtual ~Checker ()
- Public Member Functions inherited from Reporter
 Reporter ()
 Reporter (ReportPrinter *printer)
virtual ~Reporter ()
void set_printer (ReportPrinter *printer)
int print_report (TReportSeverity severity, const std::wstring &message)
- Public Member Functions inherited from HMscChecker
virtual ~HMscChecker ()

Static Public Member Functions

static LivelockCheckerPtr instance ()

Protected Member Functions

HMscPtr create_counter_example (const MscElementPListList &to_cycle, MscElementPList cycle)
- Protected Member Functions inherited from HMscChecker
 HMscChecker ()

Static Protected Attributes

static LivelockCheckerPtr m_instance

Additional Inherited Members

- Public Types inherited from Checker
typedef std::vector
< PrerequisiteCheck
 List of properties that must be satisfied before executing the check. More...

Detailed Description

LivelockChecker goes throw hmsc using traverser looking for end nodes to maek all nodes on the way backwards reachable ( mark_reachable()). Then goes again looking for circle (gray listener) that is not reachable.

Definition at line 137 of file livelock_checker.h.

Constructor & Destructor Documentation

LivelockChecker::LivelockChecker ( )

Definition at line 115 of file livelock_checker.cpp.

Referenced by instance().

LivelockChecker::~LivelockChecker ( )

Definition at line 133 of file livelock_checker.cpp.

References cleanup_attributes().

Member Function Documentation

std::list< HMscPtr > LivelockChecker::check ( HMscPtr  hmsc,
ChannelMapperPtr  mapper 

Checks HMsc against specific property.

Returns a list of MscPathPtr with violating examples if there are any in hmsc otherwise the list is empty.

hmsc- HMsc to be checked
mapper- ChannelMapper which is chosen as delivery semantic

Implements HMscChecker.

Definition at line 34 of file livelock_checker.cpp.

References ElementaryCyclesTraverser::add_cycle_listener(), DFSListenersContainer::add_white_node_found_listener(), DFSHMscTraverser::cleanup_traversing_attributes(), create_counter_example(), ElementaryCyclesTraverser::enable_restriction(), DFSBMscGraphTraverser::get_reached_elements(), DFSListenersContainer::remove_all_listeners(), result, ElementaryCyclesTraverser::traverse(), and DFSBMscGraphTraverser::traverse().

void LivelockChecker::cleanup_attributes ( )

Removes no more needed attributes.

Descendat of this class should remove attributes of MscElements that are no more needed. This method should be called after finish of algorithm.

Implements Checker.

Definition at line 138 of file livelock_checker.cpp.

Referenced by ~LivelockChecker().

HMscPtr LivelockChecker::create_counter_example ( const MscElementPListList to_cycle,
MscElementPList  cycle 
virtual std::wstring LivelockChecker::get_help_filename ( ) const

Ralative path to a HTML file displayed as help.

Implements Checker.

Definition at line 161 of file livelock_checker.h.

Checker::PreconditionList LivelockChecker::get_preconditions ( MscPtr  msc) const

Returns a list of preconditions for the check.

Implements Checker.

Definition at line 27 of file livelock_checker.cpp.

References PrerequisiteCheck::PP_REQUIRED.

virtual std::wstring LivelockChecker::get_property_name ( ) const

Human readable name of the property being checked.

Implements Checker.

Definition at line 155 of file livelock_checker.h.

LivelockCheckerPtr LivelockChecker::instance ( )

Definition at line 121 of file livelock_checker.cpp.

References LivelockChecker(), and m_instance.

bool LivelockChecker::is_supported ( ChannelMapperPtr  chm)

Checks whether Checker supports given ChannelMapper.

Deafult behaviour is false for all mappers, but it is neccessary to check out this behaviour in individual checkers.

Implements Checker.

Definition at line 128 of file livelock_checker.cpp.

Member Data Documentation

LivelockCheckerPtr LivelockChecker::m_instance

Common instance

Definition at line 143 of file livelock_checker.h.

Referenced by instance().

The documentation for this class was generated from the following files: Logo
Generated on Fri Jan 15 2016 16:26:58 for Sequence Chart Studio by  doxygen