faudes::SccFilter Class Reference

#include <cfl_graphfncts.h>

Public Types
enum	FMode {   FmNoFilter =0x00 , FmFindFirst =0x01 , FmIgnoreTrivial =0x02 , FmStatesAvoid =0x10 ,   FmStatesRequire =0x20 , FmEventsAvoid =0x40 , FmIgnoreLiveLocks =0x1000 , FmLiveLocksOnly =0x2000 ,   FmIgnoreUnaccessible =0x4000 }

Public Member Functions
	SccFilter (void)
	SccFilter (const SccFilter &rSrc)
	SccFilter (int mode, const Generator &rGen)
	SccFilter (int mode, const StateSet &rStatesAvoidRequire)
	SccFilter (int mode, const StateSet &rStatesAvoid, const StateSet &rStatesRequire)
	SccFilter (int mode, const EventSet &rEventsAvoid)
	SccFilter (int mode, const StateSet &rStatesAvoid, const StateSet &rStatesRequire, const EventSet &rEventsAvoid)
	~SccFilter (void)
int	Mode (void) const
const StateSet &	StatesAvoid (void) const
const StateSet &	StatesRequire (void) const
void	Clear (void)
void	StatesAvoid (const StateSet &rStatesAvoid)
void	StatesRequire (const StateSet &rStatesRequire)
void	EventsAvoid (const EventSet &rEventsAvoid)
void	IgnoreTrivial (bool flag)
void	FindFirst (bool flag)

Protected Member Functions
void	MergeStatesAvoid (const StateSet &rStatesAvoid)

Protected Attributes
int	mMode
const StateSet *	pStatesAvoid
const StateSet *	pStatesRequire
const EventSet *	pEventsAvoid
StateSet *	mpStatesAvoid
StateSet *	mpStatesRequire
EventSet *	mpEventsAvoid

Static Protected Attributes
static const StateSet	msEmptyStates =StateSet()
static const EventSet	msEmptyEvents =EventSet()

Friends
FAUDES_API void	SearchScc (const Idx vState, int &vRcount, const Generator &rGen, const SccFilter &rFilter, StateSet &rTodo, std::stack< Idx > &rStack, StateSet &rStackStates, std::map< const Idx, int > &rDfn, std::map< const Idx, int > &rLowLnk, std::list< StateSet > &rSccList, StateSet &rRoots)
FAUDES_API bool	ComputeNextScc (const Generator &rGen, SccFilter &rFilter, StateSet &rScc)

Detailed Description

Filter for strictly connected components (SCC) search/compute routines.

When ComputeScc()/HasScc()/NextScc() traverse a specified transition sytem in their search, a SccFilter parameter can mute certain transitions. The respective filter conditions are set by the constructor and consist of a flag word (mMode) and additional parameters (depending on the flags). The Flags can be combined from the following:

• NoFilter: std textbook beheviour;
• FindFirst: stop the search after one SCC has been found;
• IgnoreTrivial: dont report singleton SCCs without selfloop;
• StatesAvoid: mute specified states from trasition structure;
• StatesRequire: dont report SCCs that fail to contain at least one state from the specified set;
• EventsAvoid: mute any transitions with an event label from the specified set.

Convenience modes set up the state related filter conditions from the set of marked states:

• IgnoreLiveLocks: set StatesRequire to the marked states of a specified Generator;
• LiveLocksOnly: set StatesAvoid to the marked states of a specified Generator;
• IgnoreUnaccessible: initialise todo list with accessible states only.

Technical note: SccFilters interally use references to condition parameters that are required to exist during the life time of the filter object.

Technical note: currently, there is no EventsRequire filter because the implementation interprets the transition relation primarily from a directed graph perspective; while StatesRequire makes sense for marked states semantics, we are not aware of any applications for a corresponding version of EventsRequire; please let us know if you require such an extension.

Definition at line 65 of file cfl_graphfncts.h.

Member Enumeration Documentation

FMode

enum faudes::SccFilter::FMode

Typedef for filter modes

Enumerator
FmNoFilter
FmFindFirst
FmIgnoreTrivial
FmStatesAvoid
FmStatesRequire
FmEventsAvoid
FmIgnoreLiveLocks
FmLiveLocksOnly
FmIgnoreUnaccessible

Definition at line 89 of file cfl_graphfncts.h.

Constructor & Destructor Documentation

SccFilter() [1/7]

faudes::SccFilter::SccFilter

(

void

)

Constructor (no filter)

Definition at line 52 of file cfl_graphfncts.cpp.

SccFilter() [2/7]

faudes::SccFilter::SccFilter

(

const SccFilter &

rSrc

)

Constructor (copy constructor)

Definition at line 64 of file cfl_graphfncts.cpp.

SccFilter() [3/7]

faudes::SccFilter::SccFilter	(	int	mode,
		const Generator &	rGen
	)

Constructor (from flags w.r.t. Generator)

Definition at line 136 of file cfl_graphfncts.cpp.

SccFilter() [4/7]

faudes::SccFilter::SccFilter	(	int	mode,
		const StateSet &	rStatesAvoidRequire
	)

Constructor (from flags and state set, either avoid or require)

Definition at line 95 of file cfl_graphfncts.cpp.

SccFilter() [5/7]

faudes::SccFilter::SccFilter	(	int	mode,
		const StateSet &	rStatesAvoid,
		const StateSet &	rStatesRequire
	)

Constructor (from flags and state sets)

Definition at line 115 of file cfl_graphfncts.cpp.

SccFilter() [6/7]

faudes::SccFilter::SccFilter	(	int	mode,
		const EventSet &	rEventsAvoid
	)

Constructor (from flags and event sets)

Definition at line 76 of file cfl_graphfncts.cpp.

SccFilter() [7/7]

faudes::SccFilter::SccFilter	(	int	mode,
		const StateSet &	rStatesAvoid,
		const StateSet &	rStatesRequire,
		const EventSet &	rEventsAvoid
	)

Constructor (from flags and sets)

~SccFilter()

faudes::SccFilter::~SccFilter

(

void

)

Destructor

Definition at line 45 of file cfl_graphfncts.cpp.

Member Function Documentation

Clear()

void faudes::SccFilter::Clear

(

void

)

Edit filter (RTI): no filter

Definition at line 165 of file cfl_graphfncts.cpp.

EventsAvoid()

void faudes::SccFilter::EventsAvoid

(

const EventSet &

rEventsAvoid

)

Edit filter (RTI): set avoid events

Definition at line 203 of file cfl_graphfncts.cpp.

FindFirst()

void faudes::SccFilter::FindFirst

(

bool

flag

)

Edit filter (RTI): find first

Definition at line 217 of file cfl_graphfncts.cpp.

IgnoreTrivial()

void faudes::SccFilter::IgnoreTrivial

(

bool

flag

)

Edit filter (RTI): ignore trivial

Definition at line 211 of file cfl_graphfncts.cpp.

MergeStatesAvoid()

void faudes::SccFilter::MergeStatesAvoid ( const StateSet &  rStatesAvoid )

protected

Edit filter (RTI): avoid states

Definition at line 195 of file cfl_graphfncts.cpp.

Mode()

int faudes::SccFilter::Mode ( void  ) const

inline

Member access

Definition at line 127 of file cfl_graphfncts.h.

StatesAvoid() [1/2]

void faudes::SccFilter::StatesAvoid

(

const StateSet &

rStatesAvoid

)

Edit filter (RTI): set avoid states

Definition at line 179 of file cfl_graphfncts.cpp.

StatesAvoid() [2/2]

const StateSet& faudes::SccFilter::StatesAvoid ( void  ) const

inline

Member access

Definition at line 130 of file cfl_graphfncts.h.

StatesRequire() [1/2]

void faudes::SccFilter::StatesRequire

(

const StateSet &

rStatesRequire

)

Edit filter (RTI): set required states

Definition at line 187 of file cfl_graphfncts.cpp.

StatesRequire() [2/2]

const StateSet& faudes::SccFilter::StatesRequire ( void  ) const

inline

Member access

Definition at line 133 of file cfl_graphfncts.h.

Friends And Related Function Documentation

ComputeNextScc

FAUDES_API bool ComputeNextScc ( const Generator &  rGen, SccFilter &  rFilter, StateSet &  rScc  )

friend

Compute next SCC

This function provides an API for the iterative computation of SCCs. It invokes SearchScc() to find the next SCC and then adds the SCC to the StatesAvoid Filter. This approach is not computationally efficient but it allows for simple Lua wrappers.

Parameters

rGen	Generator under investigation
rFilter	Filter out specified transitions
rScc	First SCC that has been found, empty if no such.

Returns

True if an SCC has been found, false if not.

Definition at line 560 of file cfl_graphfncts.cpp.

SearchScc

FAUDES_API void SearchScc ( const Idx  vState, int &  vRcount, const Generator &  rGen, const SccFilter &  rFilter, StateSet &  rTodo, std::stack< Idx > &  rStack, StateSet &  rStackStates, std::map< const Idx, int > &  rDfn, std::map< const Idx, int > &  rLowLnk, std::list< StateSet > &  rSccList, StateSet &  rRoots  )

friend

Search for strongly connected components (SCC).

This function partitions the stateset of a generator into equivalent classes such that states x1 and x2 are equivalent iff there is a path from x1 to x2 AND a path from x2 to x1.

This function implements the algorithm based on a recursive depth first search presented in:

– Aho, Hopcroft, Ullman: The Design and Analysis of Computer Algorithms –

While the original algorithm works on a directed graph, this implementation adds some features that refer to transition systems and allow to filter SCCs on the run. The filter condition is specified by the SccFilter parameter rFilter.

Note: this version is derived from earlier implementations used in various plug-ins; in due course, this version will replace earlier versions.

Note: Due to the recursive implementation, this function requires a stack size proportional to the largest SCC. We have experienced typical default configurations to be good for a depth of about 80000 (Mac OSX 10.6, Debian 7.4). For SCCs exceeding the default stack size, you may adjust the operating system parameters accordingly. On Unix/Linux/MacOsX this is done by the shell command "ulimit -s hard". A future revision of SearchSCC() may be re-designed to circumvent this inconvenient issue.

Note: for a convenience API see also ComputeScc()

Parameters

vState	State, from which the current recursion is started.
vRcount	Denotes the current depth of the recursion.
rGen	Transition system to investigate
rFilter	Filter out specified transitions
rTodo	Set of states that up to now were not found by the depth first search.
rStack	Stack of states to represent current path.
rStackStates	Set of states that are in rStack
rDfn	Map assigning to each state idx its Depth-First Number.
rLowLnk	Map assigning to each state its LOWLINK Number.
rSccList	Set SCCs (accumulative result).
rRoots	Set of states that each are root of some SCC (accumulative result).

Definition at line 228 of file cfl_graphfncts.cpp.

Member Data Documentation

mMode

int faudes::SccFilter::mMode

protected

Flag, combining bit masks from Mode

Definition at line 160 of file cfl_graphfncts.h.

mpEventsAvoid

EventSet* faudes::SccFilter::mpEventsAvoid

protected

Definition at line 171 of file cfl_graphfncts.h.

mpStatesAvoid

StateSet* faudes::SccFilter::mpStatesAvoid

protected

Local sets (optional)

Definition at line 169 of file cfl_graphfncts.h.

mpStatesRequire

StateSet* faudes::SccFilter::mpStatesRequire

protected

Definition at line 170 of file cfl_graphfncts.h.

msEmptyEvents

const EventSet faudes::SccFilter::msEmptyEvents =EventSet()

staticprotected

Definition at line 175 of file cfl_graphfncts.h.

msEmptyStates

const StateSet faudes::SccFilter::msEmptyStates =StateSet()

staticprotected

Static emptysets

Definition at line 174 of file cfl_graphfncts.h.

pEventsAvoid

const EventSet* faudes::SccFilter::pEventsAvoid

protected

Events to avoid (if flag EventssAvoid is set)

Definition at line 166 of file cfl_graphfncts.h.

pStatesAvoid

const StateSet* faudes::SccFilter::pStatesAvoid

protected

States to avoid (if flag StatesAvoid is set)

Definition at line 162 of file cfl_graphfncts.h.

pStatesRequire

const StateSet* faudes::SccFilter::pStatesRequire

protected

States to require (if flag StatesRequire is set)

Definition at line 164 of file cfl_graphfncts.h.

---

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

• cfl_graphfncts.h
• cfl_graphfncts.cpp