30   StateSet::Iterator lit;
 
   41   FD_DF(
"UniqueInit: introducing new initial state: " << inituni);
 
   43   FD_DF(
"UniqueInit: introduce outgoing transitions: ");
 
   47       FD_DF(
"UniqueInit:   " << inituni << 
"-" << tit->Ev << 
"-" << tit->X2);
 
   53     FD_DF(
"UniqueInit: set marked state: " << inituni);
 
   70   std::vector<StateSet> power_states;
 
   71   std::vector<Idx> det_states;
 
   81     pResGen= rResGen.
New();
 
   88   if(pResGen != &rResGen) {
 
   89     pResGen->
Move(rResGen);
 
   99   rEntryStatesMap.clear();
 
  101   std::vector<StateSet> power_states;
 
  102   std::vector<Idx> det_states;
 
  106   std::vector<StateSet>::size_type i;
 
  107   for (i = 0; i < power_states.size(); ++i) {
 
  108     rEntryStatesMap.insert(std::pair<Idx,StateSet>(det_states[i], power_states[i]));
 
  114        std::vector<Idx>& rDetStates, 
Generator& rResGen) {
 
  119   FD_DF(
"Deterministic(): core function #" << rGen.
Size());
 
  123   if(&rResGen== &rGen) {
 
  124     pResGen= rResGen.
New();
 
  129   rPowerStates.clear();
 
  136   FD_DF(
"Deterministic B");
 
  140     if(pResGen != &rResGen) {
 
  141       pResGen->
Move(rResGen);
 
  144     FD_DF(
"Deterministic(): done (empty)"); 
 
  149   typedef std::multimap< Idx,std::vector<StateSet>::size_type > T_HASHMAP;
 
  151   std::vector<StateSet>::size_type current_vecindex;
 
  152   std::pair< std::map<StateSet,Idx>::iterator,
bool > result;
 
  155   StateSet::Iterator lit;
 
  156   const Idx max_idx = std::numeric_limits<Idx>::max();
 
  169       FD_DF(
"Deterministic: setting as mstate: " << rGen.
SStr(newstate));
 
  172   FD_DF(
"Deterministic: created subset of initial states {" 
  173   << newset.
ToString() << 
"} with deterministic state index " 
  174   << rGen.
SStr(newstate));
 
  176   rPowerStates.push_back(newset);
 
  177   rDetStates.push_back(newstate);
 
  178   hashmap.insert(std::make_pair(newset.
Signature(), (
Idx)rPowerStates.size() - 1));
 
  181   for (current_vecindex = 0; current_vecindex < rPowerStates.size(); 
 
  182        ++current_vecindex) {
 
  183     FD_WPC(current_vecindex,rPowerStates.size(), 
"Deterministic(): current/size: "<<  current_vecindex << 
" / " << rPowerStates.size());
 
  184     FD_DF(
"Deterministic: current power set: {"  
  185     << rPowerStates[current_vecindex].ToString() << 
"} -> "  
  186     << rDetStates[current_vecindex]);
 
  188     std::vector<StateSet> newset_vec;
 
  189     std::vector<Idx> event_vec;
 
  192     FD_DF(
"Deterministic: starting multiway merge...");
 
  193     std::list<TransSet::Iterator> merge_iterators;
 
  194     std::vector<Transition> trans_vec;
 
  198     for (lit = rPowerStates[current_vecindex].Begin(); 
 
  199    lit != rPowerStates[current_vecindex].End(); ++lit) {
 
  202   merge_iterators.push_back(tit);
 
  203   FD_DF(
"Deterministic: added merge iterator: " << rGen.
SStr(tit->X1) 
 
  204         << 
"-" << rGen.
EStr(tit->Ev) << 
"-" << rGen.
SStr(tit->X2));
 
  209     while (! merge_iterators.empty()) {
 
  210       Idx currentevent = max_idx;
 
  211       std::list<TransSet::Iterator>::iterator i; 
 
  212       std::list<TransSet::Iterator>::iterator currentit = merge_iterators.end();
 
  213       for (i = merge_iterators.begin(); i != merge_iterators.end(); ++i) {
 
  214   if ((*i)->Ev < currentevent) {
 
  215     currentevent = (*i)->Ev;
 
  229       while (currentit != merge_iterators.end()) {
 
  230   currentstate = (*currentit)->X1;
 
  234     if (j == transrel_end) {
 
  235       merge_iterators.erase(currentit++);
 
  239     else if (j->X1 == currentstate) {
 
  241       if (j->Ev == currentevent) {
 
  242         trans_vec.push_back(*j); 
 
  243         FD_DF(
"Deterine: adding transition to list: "  
  244         << rGen.
SStr(j->X1) << 
"-" << rGen.
EStr(j->Ev) << 
"-" 
  245         << rGen.
SStr(j->X2));
 
  255       merge_iterators.erase(currentit++);
 
  264     FD_DF(
"Deterministic: partitioning the transition vector...");
 
  265     std::vector<Transition>::iterator tv_it;
 
  268     for (tv_it = trans_vec.begin(); tv_it != trans_vec.end(); ++tv_it) {
 
  269       if ((tv_it->Ev == lastevent) || (lastevent == 0)) {
 
  271   lastevent = tv_it->Ev;
 
  275         << 
"} with event " << rGen.
EStr(lastevent));
 
  276   newset_vec.push_back(newset);
 
  277   event_vec.push_back(lastevent);
 
  280   lastevent = tv_it->Ev;
 
  283     if (! newset.
Empty()) {
 
  285       << 
"} with event " << rGen.
EStr(lastevent));
 
  286       newset_vec.push_back(newset);
 
  287       event_vec.push_back(lastevent);
 
  289     FD_DF(
"Deterministic: partitioning the transition vector finished");
 
  290     FD_DF(
"Deterministic: multiway merge finished");
 
  294     std::vector<StateSet>::size_type nsv_index;
 
  295     for (nsv_index = 0; nsv_index < newset_vec.size(); ++nsv_index) {
 
  296       StateSet& currentset = newset_vec[nsv_index];
 
  297       Idx currentevent = event_vec[nsv_index];
 
  301       std::pair<T_HASHMAP::iterator,T_HASHMAP::iterator> phit
 
  302   = hashmap.equal_range(sig);
 
  303       T_HASHMAP::iterator hit = phit.first;
 
  304       for (hit = phit.first; hit != phit.second; ++hit) {
 
  306   if (currentset == rPowerStates[hit->second]) {
 
  307     tmp_x2 = rDetStates[hit->second];
 
  317   rPowerStates.push_back(currentset);
 
  318   rDetStates.push_back(tmp_x2);
 
  319   hashmap.insert(std::make_pair(sig, (
Idx)rPowerStates.size() - 1));
 
  320   FD_DF(
"Deterministic: added new state "  
  322         << 
" for new subset {" << currentset.
ToString() << 
"}");
 
  324   for (lit = currentset.
Begin(); lit != currentset.
End(); ++lit) {
 
  332       pResGen->
SetTransition(rDetStates[current_vecindex], currentevent, tmp_x2);
 
  339     FD_DF(
"Deterministic: fixing names...");
 
  341     std::vector<StateSet>::size_type i;
 
  343     std::vector<Idx>::const_iterator dit;
 
  344     for (i = 0; i < rPowerStates.size(); ++i) {
 
  346       std::string name = 
"{";
 
  347       for (lit = rPowerStates[i].Begin();  lit != rPowerStates[i].End(); ++lit) {
 
  351       name.erase(name.length() - 1);
 
  353       FD_DF(
"Deterministic: setting state name \"" << name << 
"\" for index " 
  360   if(pResGen != &rResGen) {
 
  361     pResGen->
Move(rResGen);
 
  365   FD_DF(
"Deterministic(): core function: done");
 
#define FD_WPC(cntnow, contdone, message)
 
const std::string & Name(void) const
 
Idx Signature(void) const
 
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
 
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
 
StateSet::Iterator InitStatesBegin(void) const
 
const TransSet & TransRel(void) const
 
bool SetTransition(Idx x1, Idx ev, Idx x2)
 
const StateSet & MarkedStates(void) const
 
void ClearInitStates(void)
 
const EventSet & Alphabet(void) const
 
virtual void Move(vGenerator &rGen)
 
virtual vGenerator & Assign(const Type &rSrc)
 
bool InitStatesEmpty(void) const
 
const StateSet & InitStates(void) const
 
TransSet::Iterator TransRelBegin(void) const
 
Idx InitStatesSize(void) const
 
virtual vGenerator * New(void) const
 
void SetInitState(Idx index)
 
std::string StateName(Idx index) const
 
TransSet::Iterator TransRelEnd(void) const
 
std::string EStr(Idx index) const
 
void SetMarkedState(Idx index)
 
virtual void EventAttributes(const EventSet &rEventSet)
 
bool StateNamesEnabled(void) const
 
StateSet::Iterator InitStatesEnd(void) const
 
std::string SStr(Idx index) const
 
bool ExistsMarkedState(Idx index) const
 
std::string UniqueStateName(const std::string &rName) const
 
void InjectAlphabet(const EventSet &rNewalphabet)
 
Iterator Begin(void) const
 
void UniqueInit(Generator &rGen)
 
void Deterministic(const Generator &rGen, Generator &rResGen)
 
void aDeterministic(const Generator &rGen, Generator &rResGen)
 
std::string ToStringInteger(Int number)
 
std::string CollapsString(const std::string &rString, unsigned int len)