54 pStatesAvoid(&msEmptyStates),
55 pStatesRequire(&msEmptyStates),
56 pEventsAvoid(&msEmptyEvents),
66 pStatesAvoid(rSrc.pStatesAvoid),
67 pStatesRequire(rSrc.pStatesRequire),
68 pEventsAvoid(rSrc.pEventsAvoid),
78 pStatesAvoid(&msEmptyStates),
79 pStatesRequire(&msEmptyStates),
80 pEventsAvoid(&msEmptyEvents),
97 pStatesAvoid(&msEmptyStates),
98 pStatesRequire(&msEmptyStates),
99 pEventsAvoid(&msEmptyEvents),
117 pStatesAvoid(&msEmptyStates),
118 pStatesRequire(&msEmptyStates),
119 pEventsAvoid(&msEmptyEvents),
138 pStatesAvoid(&msEmptyStates),
139 pStatesRequire(&msEmptyStates),
140 pEventsAvoid(&msEmptyEvents),
234 std::stack<Idx>& rStack,
236 std::map<const Idx, int>& rDfn,
237 std::map<const Idx, int>& rLowLnk,
238 std::list<StateSet>& rSccList,
241 FD_DF(
"SerchScc: -- recursive search from state "<< vState <<
" at level " << vRcount <<
" --");
253 if(!rSccList.empty())
return;
255 rDfn[vState]=vRcount;
256 rLowLnk[vState]=vRcount;
261 rStackStates.
Insert(vState);
268 if(tit->X1!=vState)
break;
280 SearchScc(ls, vRcount, rGen, rFilter, rTodo, rStack, rStackStates, rDfn, rLowLnk, rSccList, rRoots);
282 if(rLowLnk[ls]<rLowLnk[vState]) rLowLnk[vState]=rLowLnk[ls];
287 if(rDfn[ls]<rDfn[vState])
289 if(rStackStates.
Exists(ls))
291 if(rDfn[ls]<rLowLnk[vState]) rLowLnk[vState]=rDfn[ls];
296 if(rLowLnk[vState]==rDfn[vState]) {
298 FD_DF(
"SearchScc: retrieving SCC from stack, root " << vState);
304 rStackStates.
Erase(ls);
307 rSccList.back().Insert(ls);
317 if((!fl) && (rSccList.back().Size()==1)) {
321 if(tit->X1!=vState)
break;
323 if(tit->X2!=vState)
continue;
336 #ifdef FAUDES_DEBUG_FUNCTION
337 FD_DF(
"SearchScc: invalidate scc for filter condition");
340 rRoots.
Erase(vState);
350 std::list<StateSet>& rSccList,
353 FD_DF(
"CompteScc(" << rGen.
Name() <<
")");
363 std::stack<Idx> stack;
366 std::map<const Idx, int> dfn;
367 std::map<const Idx, int> lowlnk;
381 while(!todostates.
Empty()) {
382 SearchScc(*todostates.
Begin(), count, rGen, rFilter, todostates, stack, stackstates,
383 dfn, lowlnk,rSccList, rRoots);
387 return !rSccList.empty();
393 std::list<StateSet>& rSccList,
396 FD_DF(
"CompteScc(" << rGen.
Name() <<
") [std]");
402 return ComputeScc(rGen,msFilter,rSccList,rRoots);
413 FD_DF(
"ComputeScc(" << rGen.
Name() <<
")");
422 std::stack<Idx> stack;
425 std::map<const Idx, int> dfn;
426 std::map<const Idx, int> lowlnk;
427 std::list<StateSet> scclist;
449 while(!todostates.
Empty()) {
450 SearchScc(*todostates.
Begin(), count, rGen, filter, todostates, stack, stackstates,
451 dfn, lowlnk, scclist, roots);
455 if(!scclist.empty()) rScc=*scclist.begin();
458 return !rScc.
Empty();
468 FD_DF(
"ComputeScc(" << rGen.
Name() <<
")");
477 std::stack<Idx> stack;
480 std::map<const Idx, int> dfn;
481 std::map<const Idx, int> lowlnk;
482 std::list<StateSet> scclist;
501 while(!todostates.
Empty()) {
502 SearchScc(*todostates.
Begin(), count, rGen, filter, todostates, stack, stackstates,
503 dfn, lowlnk, scclist, roots);
507 if(!scclist.empty()) rScc=*scclist.begin();
510 return !rScc.
Empty();
518 FD_DF(
"HasScc(" << rGen.
Name() <<
") [boolean only]");
524 std::stack<Idx> stack;
527 std::map<const Idx, int> dfn;
528 std::map<const Idx, int> lowlnk;
529 std::list<StateSet> scclist;
548 while(!todostates.
Empty()) {
549 SearchScc(*todostates.
Begin(), count, rGen, filter, todostates, stack, stackstates,
550 dfn, lowlnk, scclist, roots);
554 return !scclist.empty();
#define FD_DF(message)
Debug: optional report on user functions.
Operations on (directed) graphs.
Idx Insert(void)
Insert new index to set.
Set of indices with symbolic names.
bool Exists(const Idx &rIndex) const
Test existence of index.
Filter for strictly connected components (SCC) search/compute routines.
void EventsAvoid(const EventSet &rEventsAvoid)
Edit filter (RTI): set avoid events.
static const StateSet msEmptyStates
Static emptysets.
const StateSet & StatesAvoid(void) const
Member access.
const StateSet & StatesRequire(void) const
Member access.
void MergeStatesAvoid(const StateSet &rStatesAvoid)
Edit filter (RTI): avoid states.
void Clear(void)
Edit filter (RTI): no filter.
int Mode(void) const
Member access.
static const EventSet msEmptyEvents
StateSet * mpStatesAvoid
Local sets (optional)
const EventSet * pEventsAvoid
Events to avoid (if flag EventssAvoid is set)
SccFilter(void)
Constructor (no filter)
~SccFilter(void)
Destructor.
int mMode
Flag, combining bit masks from Mode.
const StateSet * pStatesAvoid
States to avoid (if flag StatesAvoid is set)
const StateSet * pStatesRequire
States to require (if flag StatesRequire is set)
StateSet * mpStatesRequire
void IgnoreTrivial(bool flag)
Edit filter (RTI): ignore trivial.
void FindFirst(bool flag)
Edit filter (RTI): find first.
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Iterator on transition.
Base class of all FAUDES generators.
const TransSet & TransRel(void) const
Return reference to transition relation.
const StateSet & MarkedStates(void) const
Return const ref of marked states.
TransSet::Iterator TransRelBegin(void) const
Iterator to Begin() of transition relation.
StateSet AccessibleSet(void) const
Compute set of accessible states.
void Name(const std::string &rName)
Set the generator's name.
TransSet::Iterator TransRelEnd(void) const
Iterator to End() of transition relation.
const StateSet & States(void) const
Return reference to state set.
void Lock(void) const
Detach and lock any further reallocation.
bool Empty(void) const
Test whether if the TBaseSet is Empty.
bool Exists(const T &rElem) const
Test existence of element.
virtual void Clear(void)
Clear all set.
virtual void InsertSet(const TBaseSet &rOtherSet)
Insert elements given by rOtherSet.
Iterator Begin(void) const
Iterator to the begin of set.
NameSet EventSet
Convenience typedef for plain event sets.
virtual bool Erase(const T &rElem)
Erase element by reference.
const std::string & Name(void) const
Return name of TBaseSet.
bool ComputeNextScc(const Generator &rGen, SccFilter &rFilter, StateSet &rScc)
Compute next SCC.
bool ComputeScc(const Generator &rGen, const SccFilter &rFilter, std::list< StateSet > &rSccList, StateSet &rRoots)
Compute strongly connected components (SCC)
bool HasScc(const Generator &rGen, const SccFilter &rFilter)
Test for strongly connected components (SCC)
libFAUDES resides within the namespace faudes.
uint32_t Idx
Type definition for index type (allways 32bit)
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)
Search for strongly connected components (SCC).