53 StateSet::Iterator lit;
60 FD_DF(
"ProjectNonDet: todo add: " << rGen.
SStr(*lit));
65 while (! todo.empty()) {
66 currentstate = todo.top();
69 FD_DF(
"ProjectNonDet: current state: " << rGen.
SStr(currentstate));
80 while(tit != tit_end) {
81 FD_DF(
"ProjectNonDet: current transition: " << rGen.
SStr(tit->X1)
82 <<
"-" << rGen.
EStr(tit->Ev) <<
"-" << rGen.
SStr(tit->X2));
83 if (! rProjectAlphabet.
Exists(tit->Ev)) {
84 FD_DF(
"ProjectNonDet: deleting current transition");
92 FD_DF(
"ProjectNonDet: relinking outgoing transitions...");
93 for (lit = reach.
Begin(); lit != reach.
End(); ++lit) {
96 for (; tit != tit_end; ++tit) {
97 if (rProjectAlphabet.
Exists(tit->Ev)) {
98 FD_DF(
"ProjectNonDet: relinking transition: " << rGen.
TStr(*tit) <<
" to " << rGen.
SStr(currentstate));
100 if (! done.
Exists(tit->X2)) {
101 FD_DF(
"ProjectNonDet: todo push: " << rGen.
SStr(tit->X2));
108 FD_DF(
"ProjectNonDet: setting marked state " << rGen.
SStr(currentstate));
131 std::stack<Idx> todod, todor;
134 StateSet::Iterator sit;
135 StateSet::Iterator sit_end;
151 while(!todod.empty()) {
154 FD_WPC(doned.
Size() - todod.size(), rGen.
Size(),
"ProjectNonDet() [STD]: done/size: "
155 << doned.
Size() - todod.size() <<
" / " << rGen.
Size());
158 currentstate = todod.top();
160 FD_DF(
"ProjectNonDet: current state: " << rGen.
SStr(currentstate));
163 todor.push(currentstate);
165 doner.
Insert(currentstate);
167 while(!todor.empty()) {
168 Idx reachstate = todor.top();
170 FD_DF(
"ProjectNonDet: reach: " << rGen.
SStr(reachstate));
176 for(; tit != tit_end; ++tit) {
177 if(tit->X1!=reachstate)
break;
179 if(rProjectAlphabet.
Exists(tit->Ev)) {
181 if(doned.
Insert(tit->X2)) {
182 FD_DF(
"ProjectNonDet: todod insert: " << rGen.
SStr(tit->X2));
188 if(doner.
Insert(tit->X2)) {
201 while(tit != tit_end) {
202 if(tit->X1!=currentstate)
break;
203 FD_DF(
"ProjectNonDet: current transition: " << rGen.
SStr(tit->X1)
204 <<
"-" << rGen.
EStr(tit->Ev) <<
"-" << rGen.
SStr(tit->X2));
205 if(!rProjectAlphabet.
Exists(tit->Ev)) {
206 FD_DF(
"ProjectNonDet: deleting current transition");
238 template<
class VLabel,
class ELabel >
struct TGraph;
239 template<
class VLabel,
class ELabel >
struct TNode;
240 template<
class VLabel,
class ELabel >
struct graph_iterator_t;
241 template<
class VLabel,
class ELabel >
struct node_iterator_t;
242 template<
class VLabel,
class ELabel >
struct node_entry_t;
261 template<
class VLabel,
class ELabel >
262 struct TGraph : std::map< VLabel , TNode< VLabel , ELabel > > {
268 return gInfX1.begin();
278 template<
class VLabel,
class ELabel >
279 struct TNode : std::set< node_entry_t< VLabel , ELabel > > {
297 template<
class VLabel,
class ELabel >
310 if(this->Ev < ent.
Ev)
return true;
311 if(this->Ev > ent.
Ev)
return false;
312 if(this->X2It->first == ent.
X2It->first)
return false;
315 return this->X2It->first < ent.
X2It->first;
326 template<
class VLabel,
class ELabel >
333 :
TGraph< VLabel , ELabel >::iterator() {}
335 :
TGraph< VLabel , ELabel >::iterator(git) {}
337 inline VLabel
X1(
void)
const {
return (*this)->first; }
339 {
return (*
FakeConst())->second.begin(); }
341 {
return (*this)->second.end(); }
343 {
return (*
FakeConst())->second.lower_bound(
346 {
return (*
FakeConst())->second.lower_bound(
351 if(x2it!=(*
this)) ++(x2it->second.RefCnt);
355 if(nit->
X2It != (*
this)) --(nit->
X2It->second.RefCnt);
356 (*this)->second.erase(nit);
359 ++((*this)->second.RefCnt);
362 inline Int UsrFlg(
void)
const {
return (*this)->second.UsrFlg; }
365 std::string
Str(
void)
const {
366 std::stringstream rep;
369 rep <<
"[" <<
X1() <<
"] ";
370 for(; nit!=nit_end; ++nit)
371 rep <<
"(" << nit.
Ev() <<
")->" << nit.
X2() <<
" ";
382 template<
class VLabel,
class ELabel >
385 :
TNode< VLabel , ELabel >::iterator() {}
387 :
TNode< VLabel , ELabel >::iterator(nit) {}
388 inline ELabel
Ev(
void)
const {
return (*this)->Ev; }
390 inline VLabel
X2(
void)
const {
return (*this)->X2It->first; }
413 return (this->insert(std::make_pair(x1,mapped_type()))).first; }
415 if(Find(x1)==End())
return false;
418 for(;git!=git_end;++git) {
421 while(nit!=nit_end) {
422 if(nit.
X2()==x1) git.
Erase(nit++);
426 return ((*this).erase(x1)) !=0;
431 if(x2it->second.RefCnt == 0 ) ((*this).erase(x2it));
439 if(git==end()) git = insert(std::make_pair(tit->X1,mapped_type())).first;
441 if(x2it==end()) x2it = insert(std::make_pair(tit->X2,mapped_type())).first;
446 for(; sit != sit_end; sit++)
447 Find(*sit).IncRefCnt();
454 for(; git != git_end; git++) {
457 for(; nit != nit_end; ++nit) {
467 std::string
Str(
void)
const {
468 std::stringstream rep;
471 for(; git!=git_end; ++git)
472 rep << git.
Str() << std::endl;
478 return gInfX1.begin(); }
493 std::stack<Graph::Iterator> todod, todor;
494 std::stack<Graph::Iterator> todov;
498 StateSet::Iterator sit;
507 FD_DF(
"ProjectNonDet: convert to graph");
509 FD_DF(
"ProjectNonDet: convert to graph: done");
513 todod.push(trg.
Find(*sit));
518 while(!todod.empty()) {
521 FD_WPC(doned.
Size() - todod.size(),trg.size(),
"ProjectNonDet() [G1]: done/size: "
522 << doned.
Size() - todod.size() <<
"/" << trg.size());
525 currentstate = todod.top();
527 FD_DF(
"ProjectNonDet: current state: " << rGen.
SStr(currentstate.
X1()));
530 todor.push(currentstate);
534 while(!todor.empty()) {
535 reachstate = todor.top();
537 FD_DF(
"ProjectNonDet: reach: " << rGen.
SStr(reachstate.
X1()));
541 nit=reachstate.
Begin();
542 nit_end=reachstate.
End();
543 for(; nit != nit_end; ++nit) {
545 if(rProjectAlphabet.
Exists(nit.
Ev())) {
547 FD_DF(
"ProjectNonDet: todod insert: " << rGen.
SStr(nit.
X2()));
548 todod.push(nit.
X2It());
551 if(reachstate!=currentstate) {
552 FD_DF(
"ProjectNonDet: trans insert: " << rGen.
SStr(currentstate.
X1()) <<
" -> " << rGen.
SStr(nit.
X2()));
559 todor.push(nit.
X2It());
560 if(nit.
X2It()==currentstate)
561 todov.push(reachstate);
570 nit=currentstate.
Begin();
571 nit_end=currentstate.
End();
572 while(nit != nit_end) {
573 if(!rProjectAlphabet.
Exists(nit.
Ev()))
574 trg.
Erase(currentstate,nit++);
583 FD_DF(
"ProjectNonDet: convert from graph");
585 FD_DF(
"ProjectNonDet: convert from graph: done");
604 std::stack<Idx> todod;
607 StateSet::Iterator sit, sit_end;
623 while(!todod.empty()) {
626 FD_WPC(doned.
Size(),rGen.
Size(),
"ProjectNonDet() [SIMPL]: current/size: "
627 << doned.
Size() <<
" / " << rGen.
Size());
630 currentstate = todod.top();
632 FD_DF(
"ProjectNonDet: current state: " << rGen.
SStr(currentstate));
638 for(; tit != tit_end; ++tit) {
639 if(!doned.
Exists(tit->X2)) { todod.push(tit->X2); doned.
Insert(tit->X2); }
640 if(rProjectAlphabet.
Exists(tit->Ev))
continue;
641 if(tit->X2==currentstate)
continue;
649 sit_end = reach.
End();
650 for(; sit != sit_end; ++sit) {
653 for(; tit != tit_end; ++tit) {
661 if(revisit) todod.push(currentstate);
665 FD_DF(
"ProjectNonDet: finalize");
688 StateSet::Iterator lit;
689 StateSet::Iterator lit2;
712 while(!todo.
Empty()) {
713 currentstate = *todo.
Begin();
715 done.
Insert(currentstate);
716 FD_DF(
"ProjectNonDet: current state: " << rGen.
SStr(currentstate));
724 FD_DF(
"ProjectNonDet: relinking outgoing transitions...");
725 for(lit = reach.
Begin(); lit != reach.
End(); ++lit) {
728 for(; tit != tit_end; ++tit) {
729 if(rProjectAlphabet.
Exists(tit->Ev)) {
730 FD_DF(
"ProjectNonDet: relinking transition: " << rGen.
TStr(*tit) <<
" to " << rGen.
SStr(currentstate));
732 if (!done.
Exists(tit->X2)) {
733 FD_DF(
"ProjectNonDet: todo insert: " << rGen.
SStr(tit->X2));
740 FD_DF(
"ProjectNonDet: local reach from state " << tit->X2 <<
": " << reachext.
ToString());
741 for (lit2 = reachext.
Begin(); lit2 != reachext.
End(); ++lit2) {
742 if (!rGen.
ExistsTransition(tit->X2, tit->Ev, *lit2) && (tit->X2 != *lit2)) {
744 FD_DF(
"ProjectNonDet: setting transition: " << rGen.
SStr(tit->X1) <<
"-" << rGen.
EStr(tit->Ev) <<
"-" << rGen.
SStr(*lit2));
746 if (!done.
Exists(*lit2)) {
747 FD_DF(
"ProjectNonDet: todo insert: " << rGen.
SStr(tit->X2));
756 FD_DF(
"ProjectNonDet: setting marked state " << rGen.
SStr(currentstate));
764 while(tit != tit_end) {
765 FD_DF(
"ProjectNonDet: current transition: " << rGen.
SStr(tit->X1)
766 <<
"-" << rGen.
EStr(tit->Ev) <<
"-" << rGen.
SStr(tit->X2));
767 if(!rProjectAlphabet.
Exists(tit->Ev)) {
768 FD_DF(
"ProjectNonDet: deleting current transition");
803 std::stack<Idx> todod, todor, todof, todox;
804 StateSet doned, doner, donef, donex;
809 StateSet::Iterator sit;
810 StateSet::Iterator sit_end;
821 FD_WPD(0,1,
"ProjectNonDet() [FB-REACH]: remove silent selfloops");
824 while(tit!=tit_end) {
825 if(tit->X1 == tit->X2)
826 if(!rProjectAlphabet.
Exists(tit->Ev))
838 while(!todod.empty()) {
841 FD_WPD(donex.
Size(), rGen.
Size(),
"ProjectNonDet() [FB-REACH]: done/size: "
842 << donex.
Size() <<
" / " << rGen.
Size());
845 currentstate = todod.top();
847 FD_DF(
"ProjectNonDet: ---- current state: " << rGen.
SStr(currentstate));
850 if(donex.
Exists(currentstate))
continue;
853 FD_DF(
"ProjectNonDet: running f-reach on " << rGen.
SStr(currentstate));
855 todor.push(currentstate);
857 doner.
Insert(currentstate);
858 Idx lastfound=currentstate;
859 while(!todor.empty()) {
860 reachstate = todor.top();
866 for(; tit != tit_end; ++tit) {
867 if(tit->X1 != reachstate)
break;
869 if(rProjectAlphabet.
Exists(tit->Ev)) {
885 if(reachstate!=currentstate) todox.push(reachstate);
890 if(donex.
Exists(currentstate))
continue;
892 FD_DF(
"ProjectNonDet: f-reach-proj found #" << doner.
Size() <<
" reachable states");
893 FD_DF(
"ProjectNonDet: f-reach-proj found #" << (donex*doner).Size() <<
" exit states");
898 FD_DF(
"ProjectNonDet: f-reach-proj found #" << candx.
Size() <<
" exit candidates");
904 FD_DF(
"ProjectNonDet: running b-reach-proj on exitstates");
905 while(!todox.empty()) {
906 exitstate = todox.top();
908 FD_DF(
"ProjectNonDet: -- b-reach on exit state: " << rGen.
SStr(exitstate));
915 for(;tit!=tit_end; ++tit) {
916 if(tit->X1!=exitstate)
break;
921 rit_end = revrel.
End();
922 while(rit != rit_end) {
923 if(rit->X2!=exitstate)
break;
929 if(donex.
Exists(rit->X1)) {++rit;
continue;}
930 FD_DF(
"ProjectNonDet: -- b-reach predecessor: " << rGen.
SStr(rit->X1));
934 for(;tit!=tit_end; ++tit)
939 FD_DF(
"unlink " << rit->Str());
942 if(!donex.
Exists(rit->X1)) {
946 while(tit != tit_end) {
947 if(rProjectAlphabet.
Exists(tit->Ev)) { ++tit;
continue;}
953 FD_DF(
"ProjectNonDet: b-reach new exit state: " << rGen.
SStr(currentstate));
956 candx.
Erase(rit->X1);
971 if(doner<=donex)
break;
975 FD_DF(
"ProjectNonDet: b-reach-proj stuck with #" << donex.
Size() <<
" exit states");
976 FD_DF(
"ProjectNonDet: choosing first of #" << candx.
Size() <<
" exit candidates");
977 exitstate= *candx.
Begin();
981 FD_DF(
"ProjectNonDet: running f-reach-proj on: " << rGen.
SStr(exitstate));
982 todof.push(exitstate);
986 while(!todof.empty()) {
987 reachstate = todof.top();
994 for(; tit != tit_end; ++tit) {
995 if(tit->X1!=reachstate)
break;
997 if(rProjectAlphabet.
Exists(tit->Ev))
1001 if(donef.
Insert(tit->X2))
1002 todof.push(tit->X2);
1006 FD_DF(
"ProjectNonDet: f-reach-proj found #" << donef.
Size() <<
" states");
1014 while(tit != tit_end) {
1015 if(tit->X1!=exitstate)
break;
1016 if(!rProjectAlphabet.
Exists(tit->Ev))
1023 #ifdef FAUDES_CHECKED
1024 if(donex.
Exists(exitstate))
1025 FD_WARN(
"ProjectNonDet: ERROR: new exit state " << exitstate);
1027 todox.push(exitstate);
1029 candx.
Erase(exitstate);
1058 std::stack<Idx> todod, todor, todof, todox;
1059 StateSet doned, doner, donef, donex;
1064 StateSet::Iterator sit;
1065 StateSet::Iterator sit_end;
1076 FD_WPD(0,1,
"ProjectNonDet() [SCC]: remove silent selfloops");
1079 while(tit!=tit_end) {
1080 if(tit->X1 == tit->X2)
1081 if(!rProjectAlphabet.
Exists(tit->Ev))
1087 FD_WPD(0,1,
"ProjectNonDet() [SCC]: compute silent sccs");
1091 std::list<StateSet> scclist;
1096 FD_WPD(0,1,
"ProjectNonDet() [SCC]: processing #" << scclist.size() <<
" sccs");
1097 std::list<StateSet>::iterator cit=scclist.begin();
1098 std::list<StateSet>::iterator cit_end=scclist.end();
1099 std::map<Idx,Idx> sccxmap;
1101 for(;cit!=cit_end;++cit) {
1102 FD_WARN(
"ProjectNonDet() [SCC]: processing scc " << cit->ToString() );
1111 for(;sit!=sit_end;++sit){
1116 while(tit!=tit_end) {
1124 if(tit->X1 != *sit)
break;
1126 if(!cit->Exists(tit->X2)) {
1131 if(rProjectAlphabet.
Exists(tit->Ev)) {
1145 for(;sit!=sit_end;++sit) sccxmap[*sit]=sccx;
1151 if(sccxmap.size()>0){
1152 FD_WPD(0,1,
"ProjectNonDet() [SCC]: applying state substitution for #" << sccxmap.size() <<
" states");
1153 std::map<Idx,Idx>::iterator xxit;
1156 while(tit!=tit_end) {
1157 xxit=sccxmap.find(tit->X2);
1158 if(xxit==sccxmap.end()) {++tit;
continue;}
1167 cit=scclist.begin();
1168 cit_end=scclist.end();
1169 for(;cit!=cit_end;++cit)
1183 while(!todod.empty()) {
1186 FD_WPD(donex.
Size(), rGen.
Size(),
"ProjectNonDet() [FB-REACH]: done/size: "
1187 << donex.
Size() <<
" / " << rGen.
Size());
1190 currentstate = todod.top();
1192 FD_DF(
"ProjectNonDet: ---- current state: " << rGen.
SStr(currentstate));
1195 if(donex.
Exists(currentstate))
continue;
1198 FD_DF(
"ProjectNonDet: running f-reach on " << rGen.
SStr(currentstate));
1200 todor.push(currentstate);
1202 doner.
Insert(currentstate);
1203 Idx lastfound=currentstate;
1204 while(!todor.empty()) {
1205 reachstate = todor.top();
1211 for(; tit != tit_end; ++tit) {
1212 if(tit->X1 != reachstate)
break;
1214 if(rProjectAlphabet.
Exists(tit->Ev)) {
1215 if(doned.
Insert(tit->X2))
1216 todod.push(tit->X2);
1223 if(doner.
Insert(tit->X2))
1224 todor.push(tit->X2);
1229 donex.
Insert(reachstate);
1230 if(reachstate!=currentstate) todox.push(reachstate);
1235 if(donex.
Exists(currentstate))
continue;
1237 FD_DF(
"ProjectNonDet: f-reach-proj found #" << doner.
Size() <<
" reachable states");
1238 FD_DF(
"ProjectNonDet: f-reach-proj found #" << (donex*doner).Size() <<
" exit states");
1243 FD_DF(
"ProjectNonDet: f-reach-proj found #" << candx.
Size() <<
" exit candidates");
1246 FD_DF(
"ProjectNonDet: running b-reach-proj on exitstates");
1247 while(!todox.empty()) {
1248 exitstate = todox.top();
1250 FD_DF(
"ProjectNonDet: -- b-reach on exit state: " << rGen.
SStr(exitstate));
1257 for(;tit!=tit_end; ++tit) {
1258 if(tit->X1!=exitstate)
break;
1263 rit_end = revrel.
End();
1264 while(rit != rit_end) {
1265 if(rit->X2!=exitstate)
break;
1271 if(donex.
Exists(rit->X1)) {++rit;
continue;}
1272 FD_DF(
"ProjectNonDet: -- b-reach predecessor: " << rGen.
SStr(rit->X1));
1275 tit_end=exits.
End();
1276 for(;tit!=tit_end; ++tit)
1281 FD_DF(
"unlink " << rit->Str());
1284 if(!donex.
Exists(rit->X1)) {
1288 while(tit != tit_end) {
1289 if(rProjectAlphabet.
Exists(tit->Ev)) { ++tit;
continue;}
1295 FD_DF(
"ProjectNonDet: b-reach new exit state: " << rGen.
SStr(currentstate));
1296 todox.push(rit->X1);
1298 candx.
Erase(rit->X1);
1306 revrel.
Erase(rit++);
1313 #ifdef FAUDES_CHECKED
1314 if(!donex.
Exists(currentstate))
1315 FD_WARN(
"ProjectNonDet: ERROR: b-reach-proj stuck with #" << donex.
Size() <<
" exit states");
1328 FD_WPD(0,1,
"ProjectNonDet() [SCC]: done");
1353 if(&rResGen != &rGen) rResGen.
Assign(rGen);
1420 if(&rResGen== &rGen) {
1421 pResGen= rResGen.
New();
1424 Project(rGen,rProjectAlphabet,*pResGen);
1428 if(pResGen != &rResGen) {
1429 pResGen->
Move(rResGen);
1438 std::map<Idx,StateSet>& rEntryStatesMap,
Generator& rResGen) {
1439 FD_DF(
"Project(...)");
1441 std::map<Idx,StateSet> tmp_entrystatemap;
1443 if(&rResGen != &rGen) rResGen.
Assign(rGen);
1450 std::vector<StateSet> subsets;
1451 std::vector<Idx> newindices;
1453 StateMin(*tmp, rResGen, subsets, newindices);
1455 std::vector<StateSet>::size_type i;
1456 std::map<Idx,StateSet>::iterator esmit;
1457 StateSet::Iterator sit;
1458 for (i = 0; i < subsets.size(); ++i) {
1460 for (sit = subsets[i].Begin(); sit != subsets[i].End(); ++sit) {
1461 esmit = tmp_entrystatemap.find(*sit);
1462 #ifdef FAUDES_DEBUG_CODE
1463 if (esmit == tmp_entrystatemap.end()) {
1464 FD_DF(
"project internal error");
1472 rEntryStatesMap.insert(std::make_pair(newindices[i], tmpstates));
1482 std::stringstream errstr;
1483 errstr <<
"Input alphabet has to contain alphabet of generator \"" << rGen.
Name() <<
"\"";
1484 throw Exception(
"InvProject(Generator,EventSet)", errstr.str(), 506);
1489 FD_DF(
"InvProject: adding events \"" << newevents.
ToString()
1490 <<
"\" at every state");
1491 StateSet::Iterator lit;
1492 EventSet::Iterator eit;
1495 for (eit = newevents.
Begin(); eit != newevents.
End(); ++eit) {
1505 FD_DF(
"aInvProject(..)");
1516 FD_DF(
"aInvProject(..): fixing attributes: source " <<
typeid(rProjectAlphabet.
AttributeType()).name() <<
1518 for(EventSet::Iterator eit=newevents.
Begin(); eit!=newevents.
End(); ++eit)
1537 std::map<Idx,StateSet>& rEntryStatesMap) {
1538 std::map<StateSet,Idx>::const_iterator it;
1539 for (it = rRevEntryStatesMap.begin(); it != rRevEntryStatesMap.end(); ++it) {
1540 rEntryStatesMap.insert(std::make_pair(it->second, it->first));
#define FD_WPC(cntnow, contdone, message)
#define FD_WPD(cntnow, cntdone, message)
bool Exists(const Idx &rIndex) const
Iterator Begin(void) const
Iterator BeginByX2(Idx x2) const
bool Insert(const Transition &rTransition)
Iterator Inject(const Iterator &pos, const Transition &rTransition)
bool Erase(const Transition &t)
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
void Write(const Type *pContext=0) const
StateSet::Iterator StatesBegin(void) const
StateSet::Iterator InitStatesBegin(void) const
bool SetTransition(Idx x1, Idx ev, Idx x2)
const EventSet & Alphabet(void) const
virtual void Move(vGenerator &rGen)
virtual vGenerator & Assign(const Type &rSrc)
const StateSet & InitStates(void) const
TransSet::Iterator TransRelBegin(void) const
void ClrTransition(Idx x1, Idx ev, Idx x2)
void InjectState(Idx index)
virtual void EventAttribute(Idx index, const Type &rAttr)
void RestrictStates(const StateSet &rStates)
void InsEvents(const EventSet &events)
virtual vGenerator * New(void) const
bool ExistsTransition(const std::string &rX1, const std::string &rEv, const std::string &rX2) const
void InjectTransition(const Transition &rTrans)
void RestrictAlphabet(const EventSet &rNewalphabet)
std::string TStr(const Transition &rTrans) const
void Name(const std::string &rName)
StateSet::Iterator StatesEnd(void) const
void DelStates(const StateSet &rDelStates)
TransSet::Iterator TransRelEnd(void) const
std::string EStr(Idx index) const
void SetMarkedState(Idx index)
virtual void EventAttributes(const EventSet &rEventSet)
void InsInitStates(const StateSet &rStates)
bool StateNamesEnabled(void) const
StateSet::Iterator InitStatesEnd(void) const
Idx TransRelSize(void) const
bool ExistsInitState(Idx index) const
std::string SStr(Idx index) const
bool ExistsMarkedState(Idx index) const
void InjectAlphabet(const EventSet &rNewalphabet)
virtual const AttributeVoid * AttributeType(void) const
bool Exists(const T &rElem) const
virtual bool AttributeTest(const Type &rAttr) const
virtual void InsertSet(const TBaseSet &rOtherSet)
Iterator Begin(void) const
virtual const AttributeVoid & Attribute(const T &rElem) const
virtual bool Erase(const T &rElem)
void StateMin(const Generator &rGen, Generator &rResGen)
void ProjectNonDetScc(Generator &rGen, const EventSet &rProjectAlphabet)
void aProjectNonDet(Generator &rGen, const EventSet &rProjectAlphabet)
bool ComputeScc(const Generator &rGen, const SccFilter &rFilter, std::list< StateSet > &rSccList, StateSet &rRoots)
void Deterministic(const Generator &rGen, Generator &rResGen)
void aInvProject(Generator &rGen, const EventSet &rProjectAlphabet)
void ProjectNonDet(Generator &rGen, const EventSet &rProjectAlphabet)
void Project(const Generator &rGen, const EventSet &rProjectAlphabet, Generator &rResGen)
void InvProject(Generator &rGen, const EventSet &rProjectAlphabet)
void aProject(const Generator &rGen, const EventSet &rProjectAlphabet, Generator &rResGen)
void LoopCallback(bool pBreak(void))
void ProjectNonDet_fbr(Generator &rGen, const EventSet &rProjectAlphabet)
void ProjectNonDet_ref(Generator &rGen, const EventSet &rProjectAlphabet)
void CreateEntryStatesMap(const std::map< StateSet, Idx > &rRevEntryStatesMap, std::map< Idx, StateSet > &rEntryStatesMap)
void ProjectNonDet_scc(Generator &rGen, const EventSet &rProjectAlphabet)
void LocalAccessibleReach(const Generator &rLowGen, const EventSet &rHighAlph, Idx lowState, StateSet &rAccessibleReach)
void ProjectNonDet_simple(Generator &rGen, const EventSet &rProjectAlphabet)
void ProjectNonDet_graph(Generator &rGen, const EventSet &rProjectAlphabet)
void ProjectNonDet_opitz(Generator &rGen, const EventSet &rProjectAlphabet)
void ProjectNonDet_barthel(Generator &rGen, const EventSet &rProjectAlphabet)
std::string CollapsString(const std::string &rString, unsigned int len)
std::string Str(void) const
static Iterator InfX1(void)
Iterator Find(Idx x1) const
Iterator End(Idx x1) const
TGraph< Idx, Idx > * FakeConst(void) const
Iterator Begin(void) const
Iterator Begin(Idx x1) const
graph_iterator_t< Idx, Idx > Iterator
void Export(vGenerator &rGen)
void Import(vGenerator &rGen)
void Erase(Iterator git, TNode< Idx, Idx >::Iterator nit)
graph_iterator_t< VLabel, ELabel > Iterator
static Iterator InfX1(void)
node_iterator_t< VLabel, ELabel > Iterator
TNode(const typename std::set< node_entry_t< VLabel, ELabel > > n)
graph_iterator_t(typename TGraph< VLabel, ELabel >::iterator git)
graph_iterator_t< VLabel, ELabel > * FakeConst(void) const
void Erase(const node_iterator_t< VLabel, ELabel > nit)
TNode< VLabel, ELabel >::Iterator End(ELabel Ev) const
TNode< VLabel, ELabel >::Iterator Begin(void) const
TNode< VLabel, ELabel >::Iterator End(void) const
bool Insert(const ELabel ev, const graph_iterator_t< VLabel, ELabel > x2it)
std::string Str(void) const
TNode< VLabel, ELabel >::Iterator Begin(ELabel Ev) const
graph_iterator_t< VLabel, ELabel > X2It
node_entry_t(ELabel ev, graph_iterator_t< VLabel, ELabel > x2it)
bool operator<(const node_entry_t< VLabel, ELabel > &ent) const
node_entry_t(const node_entry_t< VLabel, ELabel > &ent)
graph_iterator_t< VLabel, ELabel > X2It(void) const
node_iterator_t(const typename TNode< VLabel, ELabel >::iterator &nit)