36   StateSet::Iterator lit;
 
   48   FD_DF(
"mtcUniqueInit: introducing new initial state: " << inituni);
 
   50   FD_DF(
"mtcUniqueInit: introduce outgoing transitions: ");
 
   54       FD_DF(
"mtcUniqueInit:   " << inituni << 
"-" << tit->Ev << 
"-" << tit->X2);
 
   62       FD_DF(
"mtcUniqueInit: set marked state: " << inituni);
 
   75   std::vector<StateSet> power_states;
 
   76   std::vector<Idx> det_states;
 
   85   rEntryStatesMap.clear();
 
   87   std::vector<StateSet> power_states;
 
   88   std::vector<Idx> det_states;
 
   92   std::vector<StateSet>::size_type i;
 
   93   for (i = 0; i < power_states.size(); ++i) {
 
   94     rEntryStatesMap.insert(std::pair<Idx,StateSet>(det_states[i], power_states[i]));
 
  100     std::vector<Idx>& rDetStates, 
MtcSystem& rResGen) {
 
  102   rResGen.
Name(
"Det(" + rGen.
Name() + 
")");
 
  105   rPowerStates.clear();
 
  115   typedef std::multimap< Idx,std::vector<StateSet>::size_type > T_HASHMAP;
 
  117   std::vector<StateSet>::size_type current_vecindex;
 
  118   std::pair< std::map<StateSet,Idx>::iterator,
bool > result;
 
  121   StateSet::Iterator lit;
 
  122   const Idx max_idx = std::numeric_limits<Idx>::max();
 
  136   FD_DF(
"mtcDeterministic: created subset of initial states {" 
  137       << newset.
ToString() << 
"} with deterministic state index " << rGen.
SStr(newstate));
 
  139   rPowerStates.push_back(newset);
 
  140   rDetStates.push_back(newstate);
 
  141   hashmap.insert(std::make_pair(newset.
Signature(), (
Idx)rPowerStates.size() - 1));
 
  144   for (current_vecindex = 0; current_vecindex < rPowerStates.size(); ++current_vecindex) {
 
  145     FD_DF(
"mtcDeterministic: current power set: {" << rPowerStates[current_vecindex].ToString() <<
 
  146         "} -> " << rDetStates[current_vecindex]);
 
  148     std::vector<StateSet> newset_vec;
 
  149     std::vector<Idx> event_vec;
 
  152     FD_DF(
"mtcDeterministic: starting multiway merge...");
 
  153     std::list<TransSet::Iterator> merge_iterators;
 
  154     std::vector<Transition> trans_vec;
 
  158     for (lit = rPowerStates[current_vecindex].Begin();
 
  159     lit != rPowerStates[current_vecindex].End(); ++lit) {
 
  162         merge_iterators.push_back(tit);
 
  163         FD_DF(
"mtcDeterministic: added merge iterator: " << rGen.
SStr(tit->X1) 
 
  164             << 
"-" << rGen.
EStr(tit->Ev) << 
"-" << rGen.
SStr(tit->X2));
 
  169     while (! merge_iterators.empty()) {
 
  170       Idx currentevent = max_idx;
 
  171       std::list<TransSet::Iterator>::iterator i;
 
  172       std::list<TransSet::Iterator>::iterator currentit = merge_iterators.end();
 
  173       for (i = merge_iterators.begin(); i != merge_iterators.end(); ++i) {
 
  174         if ((*i)->Ev < currentevent) {
 
  175           currentevent = (*i)->Ev;
 
  189       while (currentit != merge_iterators.end()) {
 
  190         currentstate = (*currentit)->X1;
 
  194           if (j == transrel_end) {
 
  195             std::list<TransSet::Iterator>::iterator tmpit = currentit;
 
  197             merge_iterators.erase(tmpit);
 
  201           else if (j->X1 == currentstate) {
 
  203             if (j->Ev == currentevent) {
 
  204               trans_vec.push_back(*j);
 
  205               FD_DF(
"Determine: adding transition to list: " << rGen.
SStr(j->X1)
 
  206                   << 
"-" << rGen.
EStr(j->Ev) << 
"-" << rGen.
SStr(j->X2));
 
  216             std::list<TransSet::Iterator>::iterator tmpit = currentit;
 
  218             merge_iterators.erase(tmpit);
 
  227     FD_DF(
"mtcDeterministic: partitioning the transition vector...");
 
  228     std::vector<Transition>::iterator tv_it;
 
  231     for (tv_it = trans_vec.begin(); tv_it != trans_vec.end(); ++tv_it) {
 
  232       if ((tv_it->Ev == lastevent) || (lastevent == 0)) {
 
  234         lastevent = tv_it->Ev;
 
  238             << 
"} with event " << rGen.
EStr(lastevent));
 
  239         newset_vec.push_back(newset);
 
  240         event_vec.push_back(lastevent);
 
  243         lastevent = tv_it->Ev;
 
  246     if (! newset.
Empty()) {
 
  248           << 
"} with event " << rGen.
EStr(lastevent));
 
  249       newset_vec.push_back(newset);
 
  250       event_vec.push_back(lastevent);
 
  252     FD_DF(
"mtcDeterministic: partitioning the transition vector finished");
 
  253     FD_DF(
"mtcDeterministic: multiway merge finished");
 
  256     std::vector<StateSet>::size_type nsv_index;
 
  257     for (nsv_index = 0; nsv_index < newset_vec.size(); ++nsv_index) {
 
  258       StateSet& currentset = newset_vec[nsv_index];
 
  259       Idx currentevent = event_vec[nsv_index];
 
  263       std::pair<T_HASHMAP::iterator,T_HASHMAP::iterator> phit
 
  264           = hashmap.equal_range(sig);
 
  265       T_HASHMAP::iterator hit = phit.first;
 
  266       for (hit = phit.first; hit != phit.second; ++hit) {
 
  268         if (currentset == rPowerStates[hit->second]) {
 
  269           tmp_x2 = rDetStates[hit->second];
 
  279         rPowerStates.push_back(currentset);
 
  280         rDetStates.push_back(tmp_x2);
 
  281         hashmap.insert(std::make_pair(sig, (
Idx)rPowerStates.size() - 1));
 
  282         FD_DF(
"mtcDeterministic: added new state " << rGen.
SStr(tmp_x2) 
 
  283             << 
" for new subset {" << currentset.
ToString() << 
"}");
 
  285         for (lit = currentset.
Begin(); lit != currentset.
End(); ++lit) {
 
  288           FD_DF(
"mtcDeterministic: setting as colored: " << rGen.
SStr(tmp_x2));
 
  292       rResGen.
SetTransition(rDetStates[current_vecindex], currentevent, tmp_x2);
 
  297     FD_DF(
"mtcDeterministic: fixing names...");
 
  299     std::vector<StateSet>::size_type i;
 
  301     std::vector<Idx>::const_iterator dit;
 
  302     for (i = 0; i < rPowerStates.size(); ++i) {
 
  304       std::string name = 
"{";
 
  305       for (lit = rPowerStates[i].Begin(); lit != rPowerStates[i].End(); ++lit) {
 
  307           name = name + rResGen.
StateName(*lit) + 
",";
 
  313       name.erase(name.length() - 1);
 
  316       FD_DF(
"mtcDeterministic: setting state name \"" << name << 
"\" for index " << rDetStates[i]);
 
  332   std::stack<Idx> todo; 
 
  335   StateSet::Iterator lit; 
 
  342     FD_DF(
"mtcProjectNonDet: todo add: " << rGen.
SStr(*lit));
 
  347   while (! todo.empty()) {
 
  348     currentstate = todo.top();
 
  350     done.
Insert(currentstate); 
 
  351     FD_DF(
"mtcProjectNonDet: current state: " << rGen.
SStr(currentstate));
 
  356     FD_DF(
"mtcProjectNonDet: local reach: " << reach.
ToString());
 
  362     while(tit != tit_end) {
 
  363       FD_DF(
"mtcProjectNonDet: current transition: " << rGen.
SStr(tit->X1)
 
  364           << 
"-" << rGen.
EStr(tit->Ev) << 
"-" << rGen.
SStr(tit->X2));
 
  365       if (! rProjectAlphabet.
Exists(tit->Ev)) {
 
  366         FD_DF(
"mtcProjectNonDet: deleting current transition");
 
  377     FD_DF(
"mtcProjectNonDet: relinking outgoing transitions...");
 
  378     for (lit = reach.
Begin(); lit != reach.
End(); ++lit) {
 
  381       for (; tit != tit_end; ++tit) {
 
  382         if (rProjectAlphabet.
Exists(tit->Ev)) {
 
  383           FD_DF(
"mtcProjectNonDet: relinking transition: " << rGen.
TStr(*tit) << 
" to " << rGen.
SStr(currentstate) << 
"--(" << rGen.
EStr(tit->Ev) << 
")-->" << rGen.
SStr(tit->X2));
 
  385           if (! done.
Exists(tit->X2)) {
 
  386             FD_DF(
"mtcProjectNonDet: todo push: " << rGen.
SStr(tit->X2));
 
  393       if (!colors.
Empty()) {
 
  394         FD_DF(
"mtcProjectNonDet: setting colored state " << rGen.
SStr(currentstate));
 
  404   EventSet::Iterator eit;
 
  405   for(eit = unused.
Begin(); eit != unused.
End(); ++eit){
 
  411   rGen.
Name(
"MtcPro(" + rGen.
Name() + 
")" );
 
  429 #ifdef FAUDES_DEBUG_FUNCTION 
  430   FD_WARN(
"mtcProject: debug out")
 
  431   copyGen.
Write(
"tmp_project_nd.gen");
 
  435 #ifdef FAUDES_DEBUG_FUNCTION 
  436   FD_WARN(
"mtcProject: debug out")
 
  437   tmp.
Write(
"tmp_project_d.gen");
 
  441 #ifdef FAUDES_DEBUG_FUNCTION 
  442   FD_WARN(
"mtcProject: debug out")
 
  443   rResGen.
Write(
"tmp_project_m.gen");
 
  448   rResGen.
Name(rResGen.
Name()+
": mtcProject");
 
  454     std::map<Idx,StateSet>& rEntryStatesMap, 
MtcSystem& rResGen) {
 
  459   std::map<Idx,StateSet> tmp_entrystatemap;
 
  469   std::vector<StateSet> subsets;
 
  470   std::vector<Idx> newindices;
 
  475   std::vector<StateSet>::size_type i;
 
  476   std::map<Idx,StateSet>::iterator esmit;
 
  477   StateSet::Iterator sit;
 
  478   for (i = 0; i < subsets.size(); ++i) {  
 
  480     for (sit = subsets[i].Begin(); sit != subsets[i].End(); ++sit) {
 
  481       esmit = tmp_entrystatemap.find(*sit);
 
  483       if (esmit == tmp_entrystatemap.end()) {
 
  484         FD_WARN(
"mtcproject internal error");
 
  492     rEntryStatesMap.insert(std::make_pair(newindices[i], tmpstates));
 
  500   if(! (rProjectAlphabet >= rGen.
Alphabet() ) ){
 
  501     std::stringstream errstr;
 
  502     errstr << 
"Input alphabet has to contain alphabet of generator \"" << rGen.
Name() << 
"\"";
 
  503     throw Exception(
"InvProject(Generator,EventSet)", errstr.str(), 506);
 
  508   FD_DF(
"mtcInvProject: adding events \"" << newevents.
ToString() << 
"\" at every state");
 
  509   StateSet::Iterator lit;
 
  510   EventSet::Iterator eit;
 
  512     for (eit = newevents.
Begin(); eit != newevents.
End(); ++eit)
 
const std::string & Name(void) const
 
Idx Signature(void) const
 
bool Exists(const Idx &rIndex) const
 
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
 
const TaEventSet< EventAttr > & Alphabet(void) const
 
bool SetTransition(Idx x1, Idx ev, Idx x2)
 
const ATransSet & TransRel(void) const
 
void InjectAlphabet(const EventSet &rNewalphabet)
 
void ClrObservable(Idx index)
 
EventSet ControllableEvents(void) const
 
void SetControllable(Idx index)
 
EventSet ForcibleEvents(void) const
 
void SetForcible(Idx index)
 
EventSet UnobservableEvents(void) const
 
void InsColors(Idx stateIndex, const ColorSet &rColors)
 
void Colors(ColorSet &rColors) const
 
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
 
void ClearInitStates(void)
 
bool InitStatesEmpty(void) const
 
void DelEvents(const EventSet &rEvents)
 
TransSet::Iterator TransRelBegin(void) const
 
void ClrTransition(Idx x1, Idx ev, Idx x2)
 
SymbolTable * EventSymbolTablep(void) const
 
Idx InitStatesSize(void) const
 
void InsEvents(const EventSet &events)
 
bool MarkedStatesEmpty(void) const
 
void SetInitState(Idx index)
 
std::string TStr(const Transition &rTrans) const
 
std::string StateName(Idx index) const
 
StateSet::Iterator StatesEnd(void) const
 
TransSet::Iterator TransRelEnd(void) const
 
std::string EStr(Idx index) const
 
void SetMarkedState(Idx index)
 
bool StateNamesEnabled(void) const
 
StateSet::Iterator InitStatesEnd(void) const
 
EventSet UsedEvents(void) const
 
EventSet UnusedEvents(void) const
 
virtual void ClrEventAttribute(Idx index)
 
std::string SStr(Idx index) const
 
std::string UniqueStateName(const std::string &rName) const
 
bool Exists(const T &rElem) const
 
virtual void InsertSet(const TBaseSet &rOtherSet)
 
Iterator Begin(void) const
 
void mtcProject(const MtcSystem &rGen, const EventSet &rProjectAlphabet, MtcSystem &rResGen)
 
void mtcInvProject(MtcSystem &rGen, const EventSet &rProjectAlphabet)
 
void mtcProjectNonDet(MtcSystem &rGen, const EventSet &rProjectAlphabet)
 
void mtcDeterministic(const MtcSystem &rGen, MtcSystem &rResGen)
 
void mtcStateMin(MtcSystem &rGen, MtcSystem &rResGen)
 
void mtcUniqueInit(MtcSystem &rGen)
 
TmtcGenerator< AttributeVoid, AttributeColoredState, AttributeCFlags, AttributeVoid > MtcSystem
 
void LocalAccessibleReach(const Generator &rLowGen, const EventSet &rHighAlph, Idx lowState, StateSet &rAccessibleReach)
 
std::string ToStringInteger(Int number)