cfl_project.cpp
Go to the documentation of this file.
1 /** @file cfl_project.cpp projection and subset construction */
2 
3 /* FAU Discrete Event Systems Library (libfaudes)
4 
5  Copyright (C) 2006 Bernd Opitz
6  Copyright (C) 2006-2014 Thomas Moor
7  Exclusive copyright is granted to Klaus Schmidt
8 
9  This library is free software; you can redistribute it and/or
10  modify it under the terms of the GNU Lesser General Public
11  License as published by the Free Software Foundation; either
12  version 2.1 of the License, or (at your option) any later version.
13 
14  This library is distributed in the hope that it will be useful,
15  but WITHOUT ANY WARRANTY; without even the implied warranty of
16  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
17  Lesser General Public License for more details.
18 
19  You should have received a copy of the GNU Lesser General Public
20  License along with this library; if not, write to the Free Software
21  Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA */
22 
23 
24 #include "cfl_project.h"
25 #include "cfl_regular.h"
26 #include "cfl_graphfncts.h"
27 #include "cfl_localgen.h"
28 #include "cfl_statemin.h"
29 #include "cfl_determin.h"
30 
31 /* turn on debugging for this file */
32 //#undef FD_DF
33 //#define FD_DF(a) FD_WARN(a);
34 
35 namespace faudes {
36 
37 
38 // Project, version 2008/12, Bernd Opitz (?) --- usef for libFAUDES up to 2009
39 // This is believed to be the original implementation by Bend Opitz, and thus might have
40 // been in use since 2006, however, the below code snipped was grabbed in 2008. The call
41 // of "LocalAccessibleReach" is elegant, however, needs to look up every state twice.
42 // In large automata, this is a relevant contribution to the computational cost.
43 // Our re-code of this algorithm saves half of the lookups (see _ref).
44 
45 // Reference, 2008/12 (original Opitz?)
46 void ProjectNonDet_opitz(Generator& rGen, const EventSet& rProjectAlphabet) {
47 
48  // HELPERS:
49  StateSet reach; // StateSet for reachable states
50  std::stack<Idx> todo; // todo stack
51  StateSet done; // done set
52  Idx currentstate; // the currently processed state
53  StateSet::Iterator lit;
55  TransSet::Iterator tit_end;
56 
57  // ALGORITHM:
58  // initialize algorithm by pushing init states on todo stack
59  for (lit = rGen.InitStatesBegin(); lit != rGen.InitStatesEnd(); ++lit) {
60  FD_DF("ProjectNonDet: todo add: " << rGen.SStr(*lit));
61  todo.push(*lit);
62  }
63 
64  // process todo stack
65  while (! todo.empty()) {
66  currentstate = todo.top();
67  todo.pop();
68  done.Insert(currentstate);
69  FD_DF("ProjectNonDet: current state: " << rGen.SStr(currentstate));
70 
71  // comp accessible reach
72  reach.Clear();
73  LocalAccessibleReach(rGen, rProjectAlphabet, currentstate, reach);
74  FD_DF("ProjectNonDet: local reach: " << reach.ToString());
75 
76  // remove all transitions that leave current state
77  // with an invisible event
78  tit = rGen.TransRelBegin(currentstate);
79  tit_end = rGen.TransRelEnd(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");
85  rGen.ClrTransition(tit++);
86  } else {
87  ++tit;
88  }
89  }
90 
91  // relink outgoing transitions
92  FD_DF("ProjectNonDet: relinking outgoing transitions...");
93  for (lit = reach.Begin(); lit != reach.End(); ++lit) {
94  tit = rGen.TransRelBegin(*lit);
95  tit_end = rGen.TransRelEnd(*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));
99  rGen.SetTransition(currentstate, tit->Ev, tit->X2);
100  if (! done.Exists(tit->X2)) {
101  FD_DF("ProjectNonDet: todo push: " << rGen.SStr(tit->X2));
102  todo.push(tit->X2);
103  }
104  }
105  }
106  // marked status test
107  if (rGen.ExistsMarkedState(*lit)) {
108  FD_DF("ProjectNonDet: setting marked state " << rGen.SStr(currentstate));
109  rGen.SetMarkedState(currentstate);
110  }
111  }
112  }
113 
114  // inject projection alphabet
115  rGen.InjectAlphabet(rProjectAlphabet);
116 
117  // set name
118  rGen.Name(CollapsString("Pro(" + rGen.Name() + ")"));
119 }
120 
121 
122 // Projection version 2014/03, Moor -- revision of original 2008 algorithm
123 // This is a re-code of the original libFAUDES project implementation, as proposed
124 // by Bernd Opitz. The Redesign takes into account the logarithmic cost of state lockups for
125 // large input data and avoids to call the subroutine LocalAccessibleReach. The performance gain
126 // is about factor 2. We use this implementationas a reference.
127 
128 void ProjectNonDet_ref(Generator& rGen, const EventSet& rProjectAlphabet) {
129 
130  // HELPERS:
131  std::stack<Idx> todod, todor; // states todo
132  StateSet doned, doner; // states done (aka have been put to todo)
133  Idx currentstate; // the currently processed state
134  StateSet::Iterator sit;
135  StateSet::Iterator sit_end;
136  TransSet::Iterator tit;
137  TransSet::Iterator tit_end;
138 
139  // NAME
140  std::string name=CollapsString("ProjectNonDet(" + rGen.Name() + ")");
141 
142  // ALGORITHM:
143 
144  // initialize todo stack by adding init states to todo
145  for(sit=rGen.InitStatesBegin(); sit!=rGen.InitStatesEnd(); ++sit) {
146  todod.push(*sit);
147  doned.Insert(*sit);
148  }
149 
150  // process main todo stack
151  while(!todod.empty()) {
152 
153  // loop callback
154  FD_WPC(doned.Size() - todod.size(), rGen.Size(), "ProjectNonDet() [STD]: done/size: "
155  << doned.Size() - todod.size() << " / " << rGen.Size());
156 
157  // get top of the stack
158  currentstate = todod.top();
159  todod.pop();
160  FD_DF("ProjectNonDet: current state: " << rGen.SStr(currentstate));
161 
162  // local reach iteration
163  todor.push(currentstate);
164  doner.Clear();
165  doner.Insert(currentstate);
166  bool marked=rGen.ExistsMarkedState(currentstate);
167  while(!todor.empty()) {
168  Idx reachstate = todor.top();
169  todor.pop();
170  FD_DF("ProjectNonDet: reach: " << rGen.SStr(reachstate));
171  //track marking
172  marked|=rGen.ExistsMarkedState(reachstate);
173  // iterate successors
174  tit = rGen.TransRelBegin(reachstate);
175  tit_end = rGen.TransRelEnd();
176  for(; tit != tit_end; ++tit) {
177  if(tit->X1!=reachstate) break;
178  // for high-level events: insert new transition, add to main todo
179  if(rProjectAlphabet.Exists(tit->Ev)) {
180  rGen.SetTransition(currentstate, tit->Ev, tit->X2);
181  if(doned.Insert(tit->X2)) {
182  FD_DF("ProjectNonDet: todod insert: " << rGen.SStr(tit->X2));
183  todod.push(tit->X2);
184  }
185  }
186  // for low-level events: add new states to local reach todo
187  else {
188  if(doner.Insert(tit->X2)) {
189  todor.push(tit->X2);
190  }
191  }
192  }
193  } // loop: local reach
194 
195  // set marking
196  if(marked) rGen.SetMarkedState(currentstate);
197 
198  // remove all silent transitions that leave current state
199  tit = rGen.TransRelBegin(currentstate);
200  tit_end = rGen.TransRelEnd();
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");
207  rGen.ClrTransition(tit++);
208  } else {
209  ++tit;
210  }
211  }
212 
213  }// outer todo loop
214 
215  // inject projection alphabet, keep Attributes
216  rGen.RestrictAlphabet(rProjectAlphabet);
217  // make accessile
218  rGen.RestrictStates(doned);
219  // set name
220  rGen.Name(name);
221 }
222 
223 
224 /**
225  * Graph data structure for transitionrelation -- EXPERIMENTAL
226  *
227  * We have encountered situations where the set based approach implies a
228  * performace penalty for large generators. This light-weight graph class
229  * is provided to investigate the situation and to compare perfromance.
230  *
231  */
232 
233 /**
234  * Forward declaration to mimique recursive typedef by
235  * templates
236  *
237  */
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;
243 
244 
245 /**
246  * A graph is modelled as a map from vertex-labels to nodes.
247  * For our use, the vertex-labels are state indicees and each
248  * node represents the transitions from the respective state.
249  *
250  * Effectively, we implement the following structure
251  * graph:
252  * map< state-index , node >
253  * node:
254  * set< node-entry >
255  * node-entry:
256  * pair < event-index , graph-iterator > >
257  *
258  * For convenience methods addressing the intended ussage, see
259  * also the below specialisation.
260  */
261 template< class VLabel, class ELabel >
262 struct TGraph : std::map< VLabel , TNode< VLabel , ELabel > > {
263  // convenience typedef
265  // global min, element
266  static inline Iterator InfX1(void) {
267  static TGraph gInfX1;
268  return gInfX1.begin();
269  }
270 };
271 
272 
273 /**
274  * A node represents the edges related to one individual vertex.
275  * For our use, a node is a state and the edges are transitions to
276  # successor states.
277  */
278 template< class VLabel, class ELabel >
279 struct TNode : std::set< node_entry_t< VLabel , ELabel > > {
280  // user data
283  // constructors
284  TNode( void )
285  : std::set< node_entry_t< VLabel , ELabel > >() , RefCnt(0) , UsrFlg(0) {}
286  TNode( const typename std::set< node_entry_t< VLabel , ELabel > > n )
287  : std::set< node_entry_t< VLabel , ELabel > >(n) ,RefCnt(0) , UsrFlg(0) {}
288  // convenience tyepdef
290 };
291 
292 
293 /**
294  * A node-entry represents one edge. For our use, this corresponds
295  * to one transition and the edge-label is the event index.
296  */
297 template< class VLabel, class ELabel >
298 struct node_entry_t {
299  // data members
300  ELabel Ev;
302  // constructors
303  node_entry_t( void ) {};
305  : Ev(ent.Ev) , X2It(ent.X2It) {};
307  : Ev(ev), X2It(x2it) {}
308  // sorting
309  inline bool operator<(const node_entry_t< VLabel , ELabel >& ent) const {
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;
313  if(this->X2It == TGraph< VLabel , ELabel >::InfX1()) return true;
314  if(ent.X2It == TGraph< VLabel , ELabel >::InfX1()) return false;
315  return this->X2It->first < ent.X2It->first;
316  }
317 };
318 
319 
320 /**
321  * An iterator over the map of all nodes is interpreted
322  * as a state incl. all related transition. This impelmentation
323  * provides convenience methods to access the state index and to iterate
324  * over exiting transitions.
325  */
326 template< class VLabel, class ELabel >
327 struct graph_iterator_t : TGraph< VLabel , ELabel >::iterator {
328  // convenience const cast
330  { return (const_cast<graph_iterator_t< VLabel , ELabel >* >(this)); }
331  // constructors
333  : TGraph< VLabel , ELabel >::iterator() {}
335  : TGraph< VLabel , ELabel >::iterator(git) {}
336  // read access
337  inline VLabel X1(void) const { return (*this)->first; }
338  inline typename TNode< VLabel , ELabel >::Iterator Begin(void) const
339  { return (*FakeConst())->second.begin(); }
340  inline typename TNode< VLabel , ELabel >::Iterator End(void) const
341  { return (*this)->second.end(); }
342  inline typename TNode< VLabel , ELabel >::Iterator Begin(ELabel Ev) const
343  { return (*FakeConst())->second.lower_bound(
344  std::make_pair(Ev , TGraph< VLabel , ELabel >::InfX1()) ); }
345  inline typename TNode< VLabel , ELabel >::Iterator End(ELabel Ev) const
346  { return (*FakeConst())->second.lower_bound(
347  std::make_pair(Ev+1 , TGraph< VLabel , ELabel >::InfX1()) ); }
348  // write access
349  inline bool Insert(const ELabel ev, const graph_iterator_t< VLabel , ELabel > x2it) {
350  if(! (*this)->second.insert(node_entry_t< VLabel , ELabel >(ev,x2it)).second) return false;
351  if(x2it!=(*this)) ++(x2it->second.RefCnt);
352  return true;
353  }
354  inline void Erase(const node_iterator_t< VLabel , ELabel > nit) {
355  if(nit->X2It != (*this)) --(nit->X2It->second.RefCnt);
356  (*this)->second.erase(nit);
357  }
358  inline void IncRefCnt(void) {
359  ++((*this)->second.RefCnt);
360  }
361  // user data
362  inline Int UsrFlg(void) const { return (*this)->second.UsrFlg; }
363  inline void UsrFlg(Int f) { (*this)->second.UsrFlg=f; }
364  // inspect for debugging
365  std::string Str(void) const {
366  std::stringstream rep;
368  typename TNode< VLabel , ELabel >::Iterator nit_end=End();
369  rep << "[" << X1() << "] ";
370  for(; nit!=nit_end; ++nit)
371  rep << "(" << nit.Ev() << ")->" << nit.X2() << " ";
372  return rep.str();
373  }
374 
375 };
376 
377 
378 /**
379  * An iterator over the set of edges related to one vertex is interpreted
380  * as a transition.
381  */
382 template< class VLabel, class ELabel >
383 struct node_iterator_t : TNode< VLabel , ELabel >::iterator {
385  : TNode< VLabel , ELabel >::iterator() {}
387  : TNode< VLabel , ELabel >::iterator(nit) {}
388  inline ELabel Ev(void) const { return (*this)->Ev; }
389  inline graph_iterator_t< VLabel , ELabel > X2It(void) const { return (*this)->X2It; }
390  inline VLabel X2(void) const { return (*this)->X2It->first; }
391 };
392 
393 
394 /**
395  * Specialisation of the graph template to provide convenience methods
396  * addressing the intended ussage.
397  */
398 template< >
399 struct TGraph<Idx,Idx> : std::map< Idx , TNode< Idx , Idx > >{
400  // convenience typedef
402  // conveniend const cast
403  inline TGraph<Idx,Idx>* FakeConst(void) const
404  { return (const_cast<TGraph< Idx, Idx>*>(this)); }
405  // read access
406  inline Iterator Begin(void) const { return FakeConst()->begin(); }
407  inline Iterator End(void) const { return FakeConst()->end(); }
408  inline Iterator Begin(Idx x1) const { return FakeConst()->lower_bound(x1); }
409  inline Iterator End(Idx x1) const { return FakeConst()->lower_bound(x1+1); }
410  inline Iterator Find(Idx x1) const { return FakeConst()->find(x1); }
411  // write access
412  inline Iterator Insert(Idx x1) {
413  return (this->insert(std::make_pair(x1,mapped_type()))).first; }
414  inline bool Erase(Idx x1) {
415  if(Find(x1)==End()) return false;
416  Iterator git=Begin();
417  Iterator git_end=End();
418  for(;git!=git_end;++git) {
420  TNode<Idx,Idx>::Iterator nit_end=git.End();
421  while(nit!=nit_end) {
422  if(nit.X2()==x1) git.Erase(nit++);
423  else ++nit;
424  }
425  }
426  return ((*this).erase(x1)) !=0; // allways true
427  }
428  inline void Erase(Iterator git, TNode<Idx,Idx>::Iterator nit) {
429  Iterator x2it = nit.X2It();
430  git.Erase(nit);
431  if(x2it->second.RefCnt == 0 ) ((*this).erase(x2it));
432  }
433  // conversion from generator interface (destructive)
434  void Import(vGenerator& rGen) {
435  TransSet::Iterator tit = rGen.TransRelBegin();
436  TransSet::Iterator tit_end = rGen.TransRelEnd();
437  for(; tit != tit_end; rGen.ClrTransition(tit++)) {
438  Iterator git=find(tit->X1);
439  if(git==end()) git = insert(std::make_pair(tit->X1,mapped_type())).first;
440  Iterator x2it=find(tit->X2);
441  if(x2it==end()) x2it = insert(std::make_pair(tit->X2,mapped_type())).first;
442  git.Insert(tit->Ev,x2it);
443  }
444  StateSet::Iterator sit = rGen.InitStatesBegin();
445  StateSet::Iterator sit_end = rGen.InitStatesEnd();
446  for(; sit != sit_end; sit++)
447  Find(*sit).IncRefCnt();
448  };
449  // conversion to generator (destructive)
450  void Export(vGenerator& rGen) {
451  rGen.ClearTransRel();
452  Iterator git=begin();
453  Iterator git_end=end();
454  for(; git != git_end; git++) {
455  TNode<Idx,Idx>::Iterator nit =git.Begin();
456  TNode<Idx,Idx>::Iterator nit_end=git.End();
457  for(; nit != nit_end; ++nit) {
458  rGen.InjectState(git.X1());
459  rGen.InjectState(nit.X2());
460  rGen.InjectTransition(Transition(git.X1(),nit.Ev(),nit.X2()));
461  }
462  git->second.clear();
463  }
464  this->clear();
465  }
466  // inspect or debugging
467  std::string Str(void) const {
468  std::stringstream rep;
469  Iterator git=Begin();
470  Iterator git_end=End();
471  for(; git!=git_end; ++git)
472  rep << git.Str() << std::endl;
473  return rep.str();
474  }
475  // global min, element
476  static inline Iterator InfX1(void) {
477  static TGraph gInfX1;
478  return gInfX1.begin(); }
479 };
480 
481 
482 // convenience typedefs
485 
486 
487 // Projection, version 2014/03, Moor -- graph based implementation of original 2008 algorithm
488 // The performance gain is about +50%, demonstrating that the graph data structure is a more
489 // adequate representation for intensive forward reachability analysis.
490 
491 void ProjectNonDet_graph(Generator& rGen, const EventSet& rProjectAlphabet) {
492 
493  std::stack<Graph::Iterator> todod, todor; // states todo
494  std::stack<Graph::Iterator> todov; // states todo
495  StateSet doned, doner; // states done (aka have been put to todo)
496  Graph::Iterator currentstate; // the currently processed state
497  Graph::Iterator reachstate; // inner reachability loop
498  StateSet::Iterator sit;
499  Graph trg;
500  Graph::Iterator git, git_end;
501  Node::Iterator nit, nit_end;
502 
503  // NAME
504  std::string name=CollapsString("ProjectNonDet(" + rGen.Name() + ")");
505 
506  // convert to graph
507  FD_DF("ProjectNonDet: convert to graph");
508  trg.Import(rGen);
509  FD_DF("ProjectNonDet: convert to graph: done");
510 
511  // initialize todo stack by adding init states to todo
512  for(sit=rGen.InitStatesBegin(); sit!=rGen.InitStatesEnd(); ++sit) {
513  todod.push(trg.Find(*sit));
514  doned.Insert(*sit);
515  }
516 
517  // process main todo stack
518  while(!todod.empty()) {
519 
520  // loop callback
521  FD_WPC(doned.Size() - todod.size(),trg.size(), "ProjectNonDet() [G1]: done/size: "
522  << doned.Size() - todod.size() << "/" << trg.size());
523 
524  // get top of the stack
525  currentstate = todod.top();
526  todod.pop();
527  FD_DF("ProjectNonDet: current state: " << rGen.SStr(currentstate.X1()));
528 
529  // local reach iteration
530  todor.push(currentstate);
531  doner.Clear();
532  doner.Insert(currentstate.X1());
533  bool marked=rGen.ExistsMarkedState(currentstate->first);
534  while(!todor.empty()) {
535  reachstate = todor.top();
536  todor.pop();
537  FD_DF("ProjectNonDet: reach: " << rGen.SStr(reachstate.X1()));
538  //track marking
539  marked|=rGen.ExistsMarkedState(reachstate.X1());
540  // iterate successors
541  nit=reachstate.Begin();
542  nit_end=reachstate.End();
543  for(; nit != nit_end; ++nit) {
544  // for high-level events: add to main todo and insert new transition,
545  if(rProjectAlphabet.Exists(nit.Ev())) {
546  if(doned.Insert(nit.X2())) {
547  FD_DF("ProjectNonDet: todod insert: " << rGen.SStr(nit.X2()));
548  todod.push(nit.X2It());
549  }
550  // transition is only new if we are not on the currentstate
551  if(reachstate!=currentstate) {
552  FD_DF("ProjectNonDet: trans insert: " << rGen.SStr(currentstate.X1()) << " -> " << rGen.SStr(nit.X2()));
553  currentstate.Insert(nit.Ev(),nit.X2It());
554  }
555  }
556  // for low-level events: add new states to reach todo
557  else {
558  if(doner.Insert(nit.X2()))
559  todor.push(nit.X2It());
560  if(nit.X2It()==currentstate)
561  todov.push(reachstate);
562  }
563  }
564  } // loop: local reach
565 
566  // set marking
567  if(marked) rGen.SetMarkedState(currentstate->first);
568 
569  // remove all silent transitions that leave current state
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++);
575  //currentstate.Erase(nit++);
576  else
577  ++nit;
578  }
579 
580  }// outer todo loop
581 
582  // convert back
583  FD_DF("ProjectNonDet: convert from graph");
584  trg.Export(rGen);
585  FD_DF("ProjectNonDet: convert from graph: done");
586 
587  // inject projection alphabet, keep Attributes
588  rGen.RestrictAlphabet(rProjectAlphabet);
589  // make accessile
590  rGen.RestrictStates(doned);
591  // set name
592  rGen.Name(name);
593 }
594 
595 
596 
597 // Projection, version 2014/03, Moor -- simple algorithm
598 // For large automata, the performance penalty is prohibitive. However, this
599 // simple variant is useful for validation of correctness for other implementations.
600 
601 void ProjectNonDet_simple(Generator& rGen, const EventSet& rProjectAlphabet) {
602 
603  // HELPERS:
604  std::stack<Idx> todod; // states todo
605  StateSet doned; // states done (aka have been put to todo)
606  Idx currentstate; // the currently processed state
607  StateSet::Iterator sit, sit_end;
608  TransSet::Iterator tit, tit_end;
609  StateSet reach;
610 
611  // NAME
612  std::string name=CollapsString("ProjectNonDet(" + rGen.Name() + ")");
613 
614  // ALGORITHM:
615 
616  // initialize todo stack by adding init states to todo
617  for(sit=rGen.InitStatesBegin(); sit!=rGen.InitStatesEnd(); ++sit) {
618  todod.push(*sit);
619  doned.Insert(*sit);
620  }
621 
622  // process main todo stack
623  while(!todod.empty()) {
624 
625  // loop callback
626  FD_WPC(doned.Size(),rGen.Size(), "ProjectNonDet() [SIMPL]: current/size: "
627  << doned.Size() << " / " << rGen.Size());
628 
629  // get top of the stack
630  currentstate = todod.top();
631  todod.pop();
632  FD_DF("ProjectNonDet: current state: " << rGen.SStr(currentstate));
633 
634  // inspect successors to obtain one-step silent reach set
635  reach.Clear();
636  tit = rGen.TransRelBegin(currentstate);
637  tit_end = rGen.TransRelEnd(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;
642  reach.Insert(tit->X2);
643  }
644 
645  // copy local successor transitions/marking to this state
646  bool revisit=false;
647  bool marked=rGen.ExistsMarkedState(currentstate);
648  sit = reach.Begin();
649  sit_end = reach.End();
650  for(; sit != sit_end; ++sit) {
651  tit = rGen.TransRelBegin(*sit);
652  tit_end = rGen.TransRelEnd(*sit);
653  for(; tit != tit_end; ++tit) {
654  revisit|=rGen.SetTransition(currentstate,tit->Ev,tit->X2);
655  marked|=rGen.ExistsMarkedState(tit->X1);
656  }
657  }
658  if(marked) rGen.InsMarkedState(currentstate);
659 
660  // queue again if we introdced a new transion
661  if(revisit) todod.push(currentstate);
662 
663  } // todo stack
664 
665  FD_DF("ProjectNonDet: finalize");
666 
667  // restrict to projection alphabet, keep Attributes
668  rGen.RestrictAlphabet(rProjectAlphabet);
669  // make accessile
670  rGen.Accessible();
671  // set name
672  rGen.Name(name);
673 }
674 
675 
676 // Project, version 2009/05, Tobias Barthel -- used for libFAUDES 2.14 to 2.23 (2009 -- 2014)
677 // Tobias Barthel found a test case (non-deterministic? diagnoser?) in which the original implementation
678 // by Bernd Opitz was believed to fail. Unfortunatly, this test case is now lost. As of 2014/03, we use
679 // the above re-coded version of the original algorithm as our reference. We believe it to be correct
680 // ... it passed all our test cases with identical results to the below implementation.
681 void ProjectNonDet_barthel(Generator& rGen, const EventSet& rProjectAlphabet) {
682 
683  // HELPERS:
684  StateSet reach, reachext; // StateSet for reachable states
685  StateSet todo; // states todo
686  StateSet done; // states done
687  Idx currentstate; // the currently processed state
688  StateSet::Iterator lit;
689  StateSet::Iterator lit2;
690  TransSet::Iterator tit;
691  TransSet::Iterator tit_end;
692 
693  // NAME
694  std::string name=CollapsString("ProjectNonDet(" + rGen.Name() + ")");
695 
696  // ALGORITHM:
697 
698  // set all locally reachable states to init states
699  // tmoor 201403: is this needed to prevent the initial state to disappear?
700  reachext.Clear();
701  for(lit = rGen.InitStatesBegin(); lit != rGen.InitStatesEnd(); ++lit) {
702  reach.Clear();
703  LocalAccessibleReach(rGen, rProjectAlphabet, *lit, reach);
704  reachext.InsertSet(reach);
705  }
706  rGen.InsInitStates(reachext);
707  FD_DF("ProjectNonDet: initial states: " << rGen.InitStates().ToString());
708  // initialize algorithm by adding init states to todo
709  todo.InsertSet(rGen.InitStates());
710 
711  // process todo stack
712  while(!todo.Empty()) {
713  currentstate = *todo.Begin();
714  todo.Erase(*todo.Begin());
715  done.Insert(currentstate); // mark as done
716  FD_DF("ProjectNonDet: current state: " << rGen.SStr(currentstate));
717 
718  // comp accessible reach
719  reach.Clear();
720  LocalAccessibleReach(rGen, rProjectAlphabet, currentstate, reach);
721  FD_DF("ProjectNonDet: local reach: " << reach.ToString());
722 
723  // relink outgoing transitions
724  FD_DF("ProjectNonDet: relinking outgoing transitions...");
725  for(lit = reach.Begin(); lit != reach.End(); ++lit) {
726  tit = rGen.TransRelBegin(*lit);
727  tit_end = rGen.TransRelEnd(*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));
731  rGen.SetTransition(currentstate, tit->Ev, tit->X2);
732  if (!done.Exists(tit->X2)) {
733  FD_DF("ProjectNonDet: todo insert: " << rGen.SStr(tit->X2));
734  todo.Insert(tit->X2);
735  }
736  // add transistions to all states in extended local reach
737  // tmoor 201308: I dont see why we need this ...
738  reachext.Clear();
739  LocalAccessibleReach(rGen, rProjectAlphabet, tit->X2, reachext);
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)) {
743  rGen.SetTransition(tit->X1, tit->Ev, *lit2);
744  FD_DF("ProjectNonDet: setting transition: " << rGen.SStr(tit->X1) << "-" << rGen.EStr(tit->Ev) << "-" << rGen.SStr(*lit2));
745  //if (!done.Exists(*lit2) && !todo.Exists(*lit2)) {
746  if (!done.Exists(*lit2)) {
747  FD_DF("ProjectNonDet: todo insert: " << rGen.SStr(tit->X2));
748  todo.Insert(*lit2);
749  }
750  }
751  }
752  }
753  }
754  // marked status test
755  if(rGen.ExistsMarkedState(*lit)) {
756  FD_DF("ProjectNonDet: setting marked state " << rGen.SStr(currentstate));
757  rGen.SetMarkedState(currentstate);
758  }
759  }
760 
761  // remove all silent transitions that leave current state
762  tit = rGen.TransRelBegin(currentstate);
763  tit_end = rGen.TransRelEnd(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");
769  rGen.ClrTransition(tit++);
770  } else {
771  ++tit;
772  }
773  }
774 
775  }// todo loop
776 
777  // restrict to projection alphabet, keep Attributes (could also use Inject here)
778  rGen.RestrictAlphabet(rProjectAlphabet);
779 
780  // make accessile
781  rGen.Accessible();
782 
783  // set name
784  rGen.Name(name);
785 
786 }
787 
788 
789 // Project, version 2014/03, Moor -- an alternative for some large generators.
790 // This argorithm is derived from the reference version. Subsequent to each forward
791 // reachablity analysis, the states at which only non-silent events are enabled
792 // are identified as must-exit-states. From those, a backward search is conducted, to
793 // introduce more must-exit-states. Idealy, this resolvs the entire foreward reach region.
794 // This is beneficial when compared to the reference algorithm, in which only the
795 // first state of the region is resolved. However, the backward reach will stuck
796 // if the forard reach region contains strongly connected components. See also the
797 // ProjectNonDet_scc variant, which addresses this issue.
798 
799 void ProjectNonDet_fbr(Generator& rGen, const EventSet& rProjectAlphabet) {
800 
801  // HELPERS:
802 
803  std::stack<Idx> todod, todor, todof, todox; // states todo
804  StateSet doned, doner, donef, donex; // states done (aka have been put to todo)
805  Idx currentstate; // the currently processed state
806  Idx reachstate; // the currently processed state in reach iteration
807  Idx exitstate; // the currently processed state in exit search iteration
808  StateSet candx;
809  StateSet::Iterator sit;
810  StateSet::Iterator sit_end;
811  TransSet::Iterator tit;
812  TransSet::Iterator tit_end;
813  TransSetX2EvX1 revrel;
815  TransSetX2EvX1::Iterator rit_end;
816 
817  // NAME
818  std::string name=CollapsString("ProjectNonDet(" + rGen.Name() + ")");
819 
820  // removing silent selfloops (to avoid trivial sccs and special cases in their treatment)
821  FD_WPD(0,1, "ProjectNonDet() [FB-REACH]: remove silent selfloops");
822  tit=rGen.TransRelBegin();
823  tit_end=rGen.TransRelEnd();
824  while(tit!=tit_end) {
825  if(tit->X1 == tit->X2)
826  if(!rProjectAlphabet.Exists(tit->Ev))
827  { rGen.ClrTransition(tit++); continue;}
828  ++tit;
829  }
830 
831  // initialize todo stack by init states
832  for(sit=rGen.InitStatesBegin(); sit!=rGen.InitStatesEnd(); ++sit) {
833  todod.push(*sit);
834  doned.Insert(*sit);
835  }
836 
837  // process main todo stack
838  while(!todod.empty()) {
839 
840  // loop callback
841  FD_WPD(donex.Size(), rGen.Size(), "ProjectNonDet() [FB-REACH]: done/size: "
842  << donex.Size() << " / " << rGen.Size());
843 
844  // get top of the stack
845  currentstate = todod.top();
846  todod.pop();
847  FD_DF("ProjectNonDet: ---- current state: " << rGen.SStr(currentstate));
848 
849  // bail out on trivial
850  if(donex.Exists(currentstate)) continue;
851 
852  // local forward reach to find exit-only states to initialize todox
853  FD_DF("ProjectNonDet: running f-reach on " << rGen.SStr(currentstate));
854  revrel.Clear(); // local reverse map
855  todor.push(currentstate);
856  doner.Clear();
857  doner.Insert(currentstate);
858  Idx lastfound=currentstate;
859  while(!todor.empty()) {
860  reachstate = todor.top();
861  todor.pop();
862  bool local=false;
863  // iterate successors
864  tit = rGen.TransRelBegin(reachstate);
865  tit_end = rGen.TransRelEnd();
866  for(; tit != tit_end; ++tit) {
867  if(tit->X1 != reachstate) break;
868  // add high-level events to main todo
869  if(rProjectAlphabet.Exists(tit->Ev)) {
870  if(doned.Insert(tit->X2))
871  todod.push(tit->X2);
872  }
873  // add low-level events to reach todo
874  else {
875  lastfound=tit->X2;
876  revrel.Insert(*tit);
877  local=true;
878  if(doner.Insert(tit->X2))
879  todor.push(tit->X2);
880  }
881  }
882  // record exit states
883  if(!local) {
884  donex.Insert(reachstate); // global
885  if(reachstate!=currentstate) todox.push(reachstate);
886  }
887  }
888 
889  // bail out on trivial
890  if(donex.Exists(currentstate)) continue;
891 
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");
894 
895  // have fallback candidate for exit states
896  candx.Clear();
897  if(!donex.Exists(lastfound)) candx.Insert(lastfound);
898  FD_DF("ProjectNonDet: f-reach-proj found #" << candx.Size() << " exit candidates");
899 
900  // alternate backward and forward analysis until currentstate is resolved
901  while(true) {
902 
903  // backward reach on exit states to re-link predecessors and to find new exit-only states
904  FD_DF("ProjectNonDet: running b-reach-proj on exitstates");
905  while(!todox.empty()) {
906  exitstate = todox.top();
907  todox.pop();
908  FD_DF("ProjectNonDet: -- b-reach on exit state: " << rGen.SStr(exitstate));
909  // a) record attributes
910  bool mark= rGen.ExistsMarkedState(exitstate);
911  // b) figure exit transitions
912  TransSet exits;
913  tit=rGen.TransRelBegin(exitstate);
914  tit_end=rGen.TransRelEnd();
915  for(;tit!=tit_end; ++tit) {
916  if(tit->X1!=exitstate) break;
917  exits.Inject(Transition(0,tit->Ev,tit->X2));
918  }
919  // c) iterate and re-link pre-decessors
920  rit = revrel.BeginByX2(exitstate);
921  rit_end = revrel.End();
922  while(rit != rit_end) {
923  if(rit->X2!=exitstate) break;
924  // skip non-local event (automatic by local/silent reverse relation)
925  //if(rProjectAlphabet.Exists(rit->Ev)) {++rit; continue;}
926  // skip states outside current forward reach (automatic by local/silent reverse relation)
927  //if(!doner.Exists(rit->X1)) {++rit; continue;}
928  // skip states that are known exit states
929  if(donex.Exists(rit->X1)) {++rit; continue;}
930  FD_DF("ProjectNonDet: -- b-reach predecessor: " << rGen.SStr(rit->X1));
931  // propagate exit links
932  tit=exits.Begin();
933  tit_end=exits.End();
934  for(;tit!=tit_end; ++tit)
935  rGen.SetTransition(rit->X1,tit->Ev,tit->X2);
936  // propagate attributes
937  if(mark) rGen.InsMarkedState(rit->X1);
938  // unlink original local transition
939  FD_DF("unlink " << rit->Str());
940  rGen.ClrTransition(*rit);
941  // test if we found a new exit state (the if is allways true because we went back by a silent event)
942  if(!donex.Exists(rit->X1)) {
943  bool local=false;
944  tit = rGen.TransRelBegin(rit->X1); // still in revrel
945  tit_end = rGen.TransRelEnd(rit->X1);
946  while(tit != tit_end) {
947  if(rProjectAlphabet.Exists(tit->Ev)) { ++tit; continue;}
948  if(tit->X2==exitstate) {revrel.Erase(*tit); rGen.ClrTransition(tit++); continue;} //optional
949  ++tit; local=true;
950  }
951  // record new exit-only states
952  if(!local) {
953  FD_DF("ProjectNonDet: b-reach new exit state: " << rGen.SStr(currentstate));
954  todox.push(rit->X1);
955  donex.Insert(rit->X1);
956  candx.Erase(rit->X1);
957  }
958  // record candidates to overcome ssc
959  else {
960  candx.Insert(rit->X1);
961  }
962  }
963  // unlink original in reverse transition
964  revrel.Erase(rit++);
965  } // examine one exits state
966 
967  } // todox
968 
969 
970  // break f-b-alternation
971  if(doner<=donex) break; // when dealt with entire local reach
972  //if(donex.Exists(currentstate)) break; // when dealt with current state
973 
974  // do one forward reach
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();
978 
979  // this is the std forward algorthm applied to the candidate exitstate
980  // (except that there is no need to feed the outer stack todod)
981  FD_DF("ProjectNonDet: running f-reach-proj on: " << rGen.SStr(exitstate));
982  todof.push(exitstate);
983  donef.Clear();
984  donef.Insert(exitstate);
985  bool marked=rGen.ExistsMarkedState(exitstate);
986  while(!todof.empty()) {
987  reachstate = todof.top();
988  todof.pop();
989  //track marking
990  marked|=rGen.ExistsMarkedState(reachstate);
991  // iterate successors
992  tit = rGen.TransRelBegin(reachstate);
993  tit_end = rGen.TransRelEnd();
994  for(; tit != tit_end; ++tit) {
995  if(tit->X1!=reachstate) break;
996  // for high-level events: insert new transition
997  if(rProjectAlphabet.Exists(tit->Ev))
998  rGen.SetTransition(exitstate, tit->Ev, tit->X2);
999  // for low-level events: add new states to f-reach todo
1000  else {
1001  if(donef.Insert(tit->X2))
1002  todof.push(tit->X2);
1003  }
1004  }
1005  } // reach
1006  FD_DF("ProjectNonDet: f-reach-proj found #" << donef.Size() << " states");
1007 
1008  // set marking
1009  if(marked) rGen.SetMarkedState(exitstate);
1010 
1011  // std forward algorithm continued - remove all silent transitions that leave exitstate
1012  tit = rGen.TransRelBegin(exitstate);
1013  tit_end = rGen.TransRelEnd();
1014  while(tit != tit_end) {
1015  if(tit->X1!=exitstate) break;
1016  if(!rProjectAlphabet.Exists(tit->Ev))
1017  rGen.ClrTransition(tit++);
1018  else
1019  ++tit;
1020  }
1021 
1022  // record new exit state
1023 #ifdef FAUDES_CHECKED
1024  if(donex.Exists(exitstate))
1025  FD_WARN("ProjectNonDet: ERROR: new exit state " << exitstate);
1026 #endif
1027  todox.push(exitstate);
1028  donex.Insert(exitstate);
1029  candx.Erase(exitstate);
1030 
1031  } // backward-forward alternation
1032 
1033  }// outer todod
1034 
1035  // inject projection alphabet, keep Attributes
1036  rGen.RestrictAlphabet(rProjectAlphabet);
1037  // make accessile
1038  rGen.RestrictStates(doned);
1039  // set name
1040  rGen.Name(name);
1041 
1042 }
1043 
1044 
1045 // Project, version 2014/03, Moor -- an alternative for some large generators.
1046 // This argorithm first substitutes each "silent strictly-connected compnent" by a
1047 // single state. The rational is that the usual forward reachalility analysis
1048 // would be applied multiple times for each such component, leading to something
1049 // close to quadratic order. Once the silent components have been eliminated,
1050 // a local backward reachability analysis can be applied, ending up with almost
1051 // linear order. Of course, the effective gain of efficiency depends on the
1052 // automata at hand --
1053 //
1054 void ProjectNonDet_scc(Generator& rGen, const EventSet& rProjectAlphabet) {
1055 
1056  // HELPERS:
1057 
1058  std::stack<Idx> todod, todor, todof, todox; // states todo
1059  StateSet doned, doner, donef, donex; // states done (aka have been put to todo)
1060  Idx currentstate; // the currently processed state
1061  Idx reachstate; // the currently processed state in reach iteration
1062  Idx exitstate; // the currently processed state in exit search iteration
1063  StateSet candx;
1064  StateSet::Iterator sit;
1065  StateSet::Iterator sit_end;
1066  TransSet::Iterator tit;
1067  TransSet::Iterator tit_end;
1068  TransSetX2EvX1 revrel;
1070  TransSetX2EvX1::Iterator rit_end;
1071 
1072  // NAME
1073  std::string name=CollapsString("ProjectNonDet(" + rGen.Name() + ")");
1074 
1075  // removing silent selfloops (to avoid trivial sccs and special cases in their treatment)
1076  FD_WPD(0,1, "ProjectNonDet() [SCC]: remove silent selfloops");
1077  tit=rGen.TransRelBegin();
1078  tit_end=rGen.TransRelEnd();
1079  while(tit!=tit_end) {
1080  if(tit->X1 == tit->X2)
1081  if(!rProjectAlphabet.Exists(tit->Ev))
1082  { rGen.ClrTransition(tit++); continue;}
1083  ++tit;
1084  }
1085 
1086  // indentify local sccs
1087  FD_WPD(0,1, "ProjectNonDet() [SCC]: compute silent sccs");
1088  SccFilter locreach(
1090  rProjectAlphabet);
1091  std::list<StateSet> scclist;
1092  StateSet sccroots;
1093  ComputeScc(rGen,locreach,scclist,sccroots);
1094 
1095  // have one substitute state for each individual scc
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;
1100  // loop individual sccs
1101  for(;cit!=cit_end;++cit) {
1102  FD_WARN("ProjectNonDet() [SCC]: processing scc " << cit->ToString() );
1103  // track attributes
1104  bool init=false;
1105  bool mark=false;
1106  // introduce substitute state
1107  Idx sccx = rGen.InsState();
1108  // iterate over all transitions that start in current scc
1109  sit=cit->Begin();
1110  sit_end=cit->End();
1111  for(;sit!=sit_end;++sit){
1112  init|= rGen.ExistsInitState(*sit);
1113  mark|= rGen.ExistsMarkedState(*sit);
1114  tit=rGen.TransRelBegin(*sit);
1115  tit_end=rGen.TransRelEnd(*sit);
1116  while(tit!=tit_end) {
1117  // subtle bug related to an STL detail (TM/TW 2018-12)
1118  // our loop inserts transitions with X1=sccx and will not invalidate tit or
1119  // tit_end (since they refer to X1-range strictly below sscx) ... except for the
1120  // specaial case where *sit happens to be is the last X1-state in the
1121  // transition relation: then tit_end points the universal invalid transition and
1122  // our insertion with X1=sscx sneaks in before tit_end ... rather than an
1123  // expensive update of tit_end we sense the special case to break the loop
1124  if(tit->X1 != *sit) break;
1125  // case a) exit this scc with any event
1126  if(!cit->Exists(tit->X2)) {
1127  rGen.SetTransition(sccx,tit->Ev,tit->X2);
1128  }
1129  // case b) remains in this scc with non-silent event
1130  else {
1131  if(rProjectAlphabet.Exists(tit->Ev)) {
1132  rGen.SetTransition(sccx,tit->Ev,sccx);
1133  }
1134  }
1135  // delete transition, increment ieterator
1136  rGen.ClrTransition(tit++);
1137  }
1138  }
1139  // propagate attributes to substitute state
1140  if(init) rGen.InsInitState(sccx);
1141  if(mark) rGen.InsMarkedState(sccx);
1142  // record substitution in map
1143  sit=cit->Begin();
1144  sit_end=cit->End();
1145  for(;sit!=sit_end;++sit) sccxmap[*sit]=sccx;
1146  }
1147 
1148  rGen.Write();
1149 
1150  // apply substitution
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;
1154  tit=rGen.TransRelBegin();
1155  tit_end=rGen.TransRelEnd();
1156  while(tit!=tit_end) {
1157  xxit=sccxmap.find(tit->X2);
1158  if(xxit==sccxmap.end()) {++tit;continue;}
1159  rGen.SetTransition(tit->X1,tit->Ev,xxit->second);
1160  rGen.ClrTransition(tit++);
1161  }
1162  }
1163 
1164 
1165  // delete scc states
1166  // (they dont have any transitions attached, this is cosmetic)
1167  cit=scclist.begin();
1168  cit_end=scclist.end();
1169  for(;cit!=cit_end;++cit)
1170  rGen.DelStates(*cit);
1171 
1172  // free men
1173  scclist.clear();
1174  sccxmap.clear();
1175 
1176  // initialize todo stack by init states
1177  for(sit=rGen.InitStatesBegin(); sit!=rGen.InitStatesEnd(); ++sit) {
1178  todod.push(*sit);
1179  doned.Insert(*sit);
1180  }
1181 
1182  // process main todo stack
1183  while(!todod.empty()) {
1184 
1185  // loop callback
1186  FD_WPD(donex.Size(), rGen.Size(), "ProjectNonDet() [FB-REACH]: done/size: "
1187  << donex.Size() << " / " << rGen.Size());
1188 
1189  // get top of the stack
1190  currentstate = todod.top();
1191  todod.pop();
1192  FD_DF("ProjectNonDet: ---- current state: " << rGen.SStr(currentstate));
1193 
1194  // bail out on trivial
1195  if(donex.Exists(currentstate)) continue;
1196 
1197  // local forward reach to find exit-only states to initialize todox
1198  FD_DF("ProjectNonDet: running f-reach on " << rGen.SStr(currentstate));
1199  revrel.Clear(); // local reverse map
1200  todor.push(currentstate);
1201  doner.Clear();
1202  doner.Insert(currentstate);
1203  Idx lastfound=currentstate;
1204  while(!todor.empty()) {
1205  reachstate = todor.top();
1206  todor.pop();
1207  bool local=false;
1208  // iterate successors
1209  tit = rGen.TransRelBegin(reachstate);
1210  tit_end = rGen.TransRelEnd();
1211  for(; tit != tit_end; ++tit) {
1212  if(tit->X1 != reachstate) break;
1213  // add high-level events to main todo
1214  if(rProjectAlphabet.Exists(tit->Ev)) {
1215  if(doned.Insert(tit->X2))
1216  todod.push(tit->X2);
1217  }
1218  // add low-level events to reach todo
1219  else {
1220  lastfound=tit->X2;
1221  revrel.Insert(*tit);
1222  local=true;
1223  if(doner.Insert(tit->X2))
1224  todor.push(tit->X2);
1225  }
1226  }
1227  // record exit states
1228  if(!local) {
1229  donex.Insert(reachstate); // global
1230  if(reachstate!=currentstate) todox.push(reachstate);
1231  }
1232  }
1233 
1234  // bail out on trivial
1235  if(donex.Exists(currentstate)) continue;
1236 
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");
1239 
1240  // have fallback candidate for exit states
1241  candx.Clear();
1242  if(!donex.Exists(lastfound)) candx.Insert(lastfound);
1243  FD_DF("ProjectNonDet: f-reach-proj found #" << candx.Size() << " exit candidates");
1244 
1245  // backward reach on exit states to re-link predecessors and to find new exit-only states
1246  FD_DF("ProjectNonDet: running b-reach-proj on exitstates");
1247  while(!todox.empty()) {
1248  exitstate = todox.top();
1249  todox.pop();
1250  FD_DF("ProjectNonDet: -- b-reach on exit state: " << rGen.SStr(exitstate));
1251  // a) record attributes
1252  bool mark= rGen.ExistsMarkedState(exitstate);
1253  // b) figure exit transitions
1254  TransSet exits;
1255  tit=rGen.TransRelBegin(exitstate);
1256  tit_end=rGen.TransRelEnd();
1257  for(;tit!=tit_end; ++tit) {
1258  if(tit->X1!=exitstate) break;
1259  exits.Inject(Transition(0,tit->Ev,tit->X2));
1260  }
1261  // c) iterate and re-link pre-decessors
1262  rit = revrel.BeginByX2(exitstate);
1263  rit_end = revrel.End();
1264  while(rit != rit_end) {
1265  if(rit->X2!=exitstate) break;
1266  // skip non-local event (automatic by local/silent reverse relation)
1267  //if(rProjectAlphabet.Exists(rit->Ev)) {++rit; continue;}
1268  // skip states outside current forward reach (automatic by local/silent reverse relation)
1269  //if(!doner.Exists(rit->X1)) {++rit; continue;}
1270  // skip states that are known exit states
1271  if(donex.Exists(rit->X1)) {++rit; continue;}
1272  FD_DF("ProjectNonDet: -- b-reach predecessor: " << rGen.SStr(rit->X1));
1273  // propagate exit links
1274  tit=exits.Begin();
1275  tit_end=exits.End();
1276  for(;tit!=tit_end; ++tit)
1277  rGen.SetTransition(rit->X1,tit->Ev,tit->X2);
1278  // propagate attributes
1279  if(mark) rGen.InsMarkedState(rit->X1);
1280  // unlink original local transition
1281  FD_DF("unlink " << rit->Str());
1282  rGen.ClrTransition(*rit);
1283  // test if we found a new exit state (the if is allways true because we went back by a silent event)
1284  if(!donex.Exists(rit->X1)) {
1285  bool local=false;
1286  tit = rGen.TransRelBegin(rit->X1); // still in revrel
1287  tit_end = rGen.TransRelEnd(rit->X1);
1288  while(tit != tit_end) {
1289  if(rProjectAlphabet.Exists(tit->Ev)) { ++tit; continue;}
1290  if(tit->X2==exitstate) {revrel.Erase(*tit); rGen.ClrTransition(tit++); continue;} //optional
1291  ++tit; local=true;
1292  }
1293  // record new exit-only states
1294  if(!local) {
1295  FD_DF("ProjectNonDet: b-reach new exit state: " << rGen.SStr(currentstate));
1296  todox.push(rit->X1);
1297  donex.Insert(rit->X1);
1298  candx.Erase(rit->X1);
1299  }
1300  // record candidates to overcome ssc
1301  else {
1302  candx.Insert(rit->X1);
1303  }
1304  }
1305  // unlink original in reverse transition
1306  revrel.Erase(rit++);
1307  } // examine one exits state
1308 
1309  } // todox
1310 
1311  // since we eliminated silent sccs, we must have doner<=donex,
1312  // and we dont need to run a forward in this routine
1313 #ifdef FAUDES_CHECKED
1314  if(!donex.Exists(currentstate))
1315  FD_WARN("ProjectNonDet: ERROR: b-reach-proj stuck with #" << donex.Size() << " exit states");
1316 #endif
1317 
1318 
1319  }// outer todod
1320 
1321  // inject projection alphabet, keep Attributes
1322  rGen.RestrictAlphabet(rProjectAlphabet);
1323  // make accessile
1324  rGen.RestrictStates(doned);
1325  // set name
1326  rGen.Name(name);
1327 
1328  FD_WPD(0,1, "ProjectNonDet() [SCC]: done");
1329 }
1330 
1331 
1332 
1333 // wrapper to choose std implementation
1334 void ProjectNonDet(Generator& rGen, const EventSet& rProjectAlphabet) {
1335  ProjectNonDet_ref(rGen, rProjectAlphabet); // (here: 2014 re-code of original -2008 algorithm)
1336  //ProjectNonDet_opitz(rGen, rProjectAlphabet); // (here: original code used -2008)
1337  //ProjectNonDet_barthel(rGen, rProjectAlphabet); // (here: implementation used 2009-2013)
1338  //ProjectNonDet_fbr(rGen, rProjectAlphabet); // (here: 2014 optimized algorithm)
1339  //ProjectNonDet_scc(rGen, rProjectAlphabet); // (here: 2014 optimized algorithm)
1340 }
1341 
1342 // wrapper to make the scc version available externally (purely cosmetic)
1343 void ProjectNonDetScc(Generator& rGen, const EventSet& rProjectAlphabet) {
1344  ProjectNonDet_scc(rGen, rProjectAlphabet); // (here: 2014 optimized algorithm)
1345 }
1346 
1347 
1348 // Project(rGen, rProjectAlphabet, rResGen&)
1349 void Project(const Generator& rGen, const EventSet& rProjectAlphabet, Generator& rResGen) {
1350  FD_DF("Project(...): #" << rGen.TransRelSize());
1351  //FAUDES_TIMER_START("");
1352  // initialize result with argument generator
1353  if(&rResGen != &rGen) rResGen.Assign(rGen);
1354  // turn off state names
1355  bool se= rResGen.StateNamesEnabled();
1356  rResGen.StateNamesEnabled(false);
1357  // project non det version
1358  ProjectNonDet(rResGen, rProjectAlphabet);
1359  // make deterministic
1360  Generator* gd = rGen.New();
1361  gd->StateNamesEnabled(false);
1362  //FAUDES_TIMER_LAP("");
1363  FD_DF("Project(...): make det #" << rResGen.TransRelSize());
1364  Deterministic(rResGen, *gd);
1365  // minimize states (tmoor 201308: this is cosmetic ...
1366  // ... and turned out expensive when iterating on an observer
1367  // stateset; hence we do it only for small generators)
1368  if(gd->Size() < 20)
1369  StateMin(*gd,rResGen);
1370  else
1371  gd->Move(rResGen);
1372  delete gd;
1373  // restore state names
1374  rResGen.StateNamesEnabled(se);
1375  // set name
1376  rResGen.Name("Project("+CollapsString(rGen.Name()+")"));
1377  //FAUDES_TIMER_LAP("");
1378  FD_DF("Project(...): done #" << rResGen.TransRelSize());
1379 
1380  /*
1381  // compare with reference implementation
1382  FD_WARN("Project(...): testing #" << rGen.TransRelSize());
1383  FAUDES_TIMER_START("");
1384  Generator gref=rGen;
1385  gref.StateNamesEnabled(false);
1386  ProjectNonDet_ref(gref, rProjectAlphabet);
1387  Generator g3;
1388  g3.StateNamesEnabled(false);
1389  FD_WARN("Project(...): make det #" << gref.Size());
1390  FAUDES_TIMER_LAP("");
1391  Deterministic(gref, g3);
1392  g3.Move(gref);
1393  FAUDES_TIMER_LAP("");
1394  // compare
1395  FD_WARN("Project(...): compare #" << gref.Size());
1396  FD_WARN("Project(...): ref<=alt " << LanguageInclusion(gref,rResGen));
1397  FD_WARN("Project(...): alt<=ref " << LanguageInclusion(rResGen,gref));
1398  if(!LanguageEquality(gref,rResGen)) throw Exception("Project(Generator,EventSet)", "TEST ERROR", 506);
1399  Generator resgen=rResGen;
1400  MarkAllStates(resgen);
1401  MarkAllStates(gref);
1402  FD_WARN("Project(...): compare closed");
1403  FD_WARN("Project(...): ref<=alt " << LanguageInclusion(gref,resgen));
1404  FD_WARN("Project(...): alt<=ref " << LanguageInclusion(resgen,gref));
1405  if(!LanguageEquality(gref,resgen)) throw Exception("Project(Generator,EventSet)", "TEST ERROR", 506);
1406  */
1407 }
1408 
1409 
1410 // wrapper
1411 void aProjectNonDet(Generator& rGen, const EventSet& rProjectAlphabet) {
1412  ProjectNonDet(rGen,rProjectAlphabet);
1413 }
1414 
1415 
1416 // Project(rGen, rProjectAlphabet, rResGen&)
1417 void aProject(const Generator& rGen, const EventSet& rProjectAlphabet, Generator& rResGen) {
1418  // prepare result to keep original alphabet
1419  Generator* pResGen = &rResGen;
1420  if(&rResGen== &rGen) {
1421  pResGen= rResGen.New();
1422  }
1423  // perform op
1424  Project(rGen,rProjectAlphabet,*pResGen);
1425  // set old attributes
1426  pResGen->EventAttributes(rGen.Alphabet());
1427  // copy result
1428  if(pResGen != &rResGen) {
1429  pResGen->Move(rResGen);
1430  delete pResGen;
1431  }
1432 }
1433 
1434 
1435 
1436 // Project(rGen, rProjectAlphabet, rEntryStatesMap&, rResGen&)
1437 void Project(const Generator& rGen, const EventSet& rProjectAlphabet,
1438  std::map<Idx,StateSet>& rEntryStatesMap, Generator& rResGen) {
1439  FD_DF("Project(...)");
1440  // temporary entry state map
1441  std::map<Idx,StateSet> tmp_entrystatemap;
1442  // temporarily assign rGen to rResGen
1443  if(&rResGen != &rGen) rResGen.Assign(rGen);
1444  // project tmp with respect to palphabet
1445  ProjectNonDet_ref(rResGen, rProjectAlphabet); // must use a version that does not add states
1446  // put deterministic result into tmp
1447  Generator* tmp = rGen.New();
1448  Deterministic(rResGen, tmp_entrystatemap, *tmp);
1449  // write entry state map for minimized generator
1450  std::vector<StateSet> subsets;
1451  std::vector<Idx> newindices;
1452  // minimize states and rewrite result to rResGen
1453  StateMin(*tmp, rResGen, subsets, newindices);
1454  // build entry state map
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) {
1459  StateSet tmpstates;
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");
1465  abort();
1466  }
1467 #endif
1468  // insert entry states in temporary StateSet
1469  tmpstates.InsertSet(esmit->second);
1470  }
1471 
1472  rEntryStatesMap.insert(std::make_pair(newindices[i], tmpstates));
1473  }
1474  delete tmp;
1475 }
1476 
1477 
1478 // InvProject(rGen&, rProjectAlphabet)
1479 void InvProject(Generator& rGen, const EventSet& rProjectAlphabet) {
1480  // test if the alphabet of the generator is included in the given alphabet
1481  if(! (rProjectAlphabet >= (EventSet) rGen.Alphabet() ) ){
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);
1485  }
1486  EventSet newevents = rProjectAlphabet - rGen.Alphabet();
1487  // insert events into generator
1488  rGen.InsEvents(newevents);
1489  FD_DF("InvProject: adding events \"" << newevents.ToString()
1490  << "\" at every state");
1491  StateSet::Iterator lit;
1492  EventSet::Iterator eit;
1493  for (lit = rGen.StatesBegin(); lit != rGen.StatesEnd(); ++lit) {
1494  LoopCallback(); // should only be an issue for very large generators
1495  for (eit = newevents.Begin(); eit != newevents.End(); ++eit) {
1496  rGen.SetTransition(*lit, *eit, *lit);
1497  }
1498  }
1499 }
1500 
1501 
1502 
1503 // InvProject(rGen&, rProjectAlphabet)
1504 void aInvProject(Generator& rGen, const EventSet& rProjectAlphabet) {
1505  FD_DF("aInvProject(..)");
1506  // see whether the generator can digest attribues
1507  if(!rGen.Alphabet().AttributeTest(*rProjectAlphabet.AttributeType())) {
1508  InvProject(rGen,rProjectAlphabet);
1509  return;
1510  }
1511  // record extra events
1512  EventSet newevents = rProjectAlphabet - rGen.Alphabet();
1513  // perform
1514  InvProject(rGen,rProjectAlphabet);
1515  // copy all attributes from input alphabets
1516  FD_DF("aInvProject(..): fixing attributes: source " << typeid(*rProjectAlphabet.AttributeType()).name() <<
1517  " dest " << typeid(*rGen.Alphabet().AttributeType()).name());
1518  for(EventSet::Iterator eit=newevents.Begin(); eit!=newevents.End(); ++eit)
1519  rGen.EventAttribute(*eit,rProjectAlphabet.Attribute(*eit));
1520 }
1521 
1522 
1523 // InvProject
1525  const Generator& rGen,
1526  const EventSet& rProjectAlphabet,
1527  Generator& rResGen)
1528 {
1529  rResGen.Assign(rGen);
1530  aInvProject(rResGen, rProjectAlphabet);
1531 }
1532 
1533 
1534 
1535 // CreateEntryStatesMap(rRevEntryStatesMap, rEntryStatesMap)
1536 void CreateEntryStatesMap(const std::map<StateSet,Idx>& rRevEntryStatesMap,
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));
1541  }
1542 }
1543 
1544 
1545 
1546 } // namespace faudes
#define FD_WPC(cntnow, contdone, message)
Application callback: optional write progress report to console or application, incl count
#define FD_WARN(message)
Debug: always report warnings.
#define FD_DF(message)
Debug: optional report on user functions.
#define FD_WPD(cntnow, cntdone, message)
Alternative progessreport for development.
powersetset construction
Operations on (directed) graphs.
Helper functions for projected generators.
language projection
Operations on regular languages.
state space minimization
Faudes exception class.
Set of indices.
Definition: cfl_indexset.h:78
Idx Insert(void)
Insert new index to set.
Set of indices with symbolic names.
Definition: cfl_nameset.h:69
bool Exists(const Idx &rIndex) const
Test existence of index.
Filter for strictly connected components (SCC) search/compute routines.
Iterator class for high-level api to TBaseSet.
Definition: cfl_baseset.h:387
Set of Transitions.
Definition: cfl_transset.h:242
Iterator Begin(void) const
Iterator to begin of set.
Iterator End(void) const
Iterator to end of set.
Iterator BeginByX2(Idx x2) const
Iterator to first Transition specified by successor state x2.
bool Insert(const Transition &rTransition)
Add a Transition.
Iterator Inject(const Iterator &pos, const Transition &rTransition)
Add a Transition.
bool Erase(const Transition &t)
Remove a Transition.
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Iterator on transition.
Definition: cfl_transset.h:269
Triple (X1,Ev,X2) to represent current state, event and next state.
Definition: cfl_transset.h:57
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
Write configuration data to a string.
Definition: cfl_types.cpp:169
void Write(const Type *pContext=0) const
Write configuration data to console.
Definition: cfl_types.cpp:139
Base class of all FAUDES generators.
StateSet::Iterator StatesBegin(void) const
Iterator to Begin() of state set.
StateSet::Iterator InitStatesBegin(void) const
Iterator to Begin() of mInitStates.
bool SetTransition(Idx x1, Idx ev, Idx x2)
Add a transition to generator by indices.
const EventSet & Alphabet(void) const
Return const reference to alphabet.
void ClearTransRel(void)
Clear all transitions.
Idx InsMarkedState(void)
Create new anonymous state and set as marked state.
virtual void Move(vGenerator &rGen)
Destructive copy to other vGenerator.
virtual vGenerator & Assign(const Type &rSrc)
Copy from other faudes type.
const StateSet & InitStates(void) const
Const ref to initial states.
TransSet::Iterator TransRelBegin(void) const
Iterator to Begin() of transition relation.
void ClrTransition(Idx x1, Idx ev, Idx x2)
Remove a transition by indices.
bool Accessible(void)
Make generator accessible.
void InjectState(Idx index)
Inject an existing state index into generators mStates Use with care! For use in performance optimize...
virtual void EventAttribute(Idx index, const Type &rAttr)
Set attribute for existing event.
void RestrictStates(const StateSet &rStates)
Restrict states Cleans mpStates, mInitStates, mMarkedStates, mpTransrel, and mpStateSymboltable.
void InsEvents(const EventSet &events)
Add new named events to generator.
virtual vGenerator * New(void) const
Construct on heap.
bool ExistsTransition(const std::string &rX1, const std::string &rEv, const std::string &rX2) const
Test for transition given by x1, ev, x2.
void InjectTransition(const Transition &rTrans)
Set transition without consistency check.
void RestrictAlphabet(const EventSet &rNewalphabet)
Restricts mpAlphabet incl removing resp.
std::string TStr(const Transition &rTrans) const
Return pretty printable transition (eg for debugging)
void Name(const std::string &rName)
Set the generator's name.
StateSet::Iterator StatesEnd(void) const
Iterator to End() of state set.
void DelStates(const StateSet &rDelStates)
Delete a set of states Cleans mpStates, mInitStates, mMarkedStates, mpTransrel, and mpStateSymboltabl...
TransSet::Iterator TransRelEnd(void) const
Iterator to End() of transition relation.
std::string EStr(Idx index) const
Pretty printable event name for index (eg for debugging).
Idx InsState(void)
Add new anonymous state to generator.
void SetMarkedState(Idx index)
Set an existing state as marked state by index.
Idx InsInitState(void)
Create new anonymous state and set as initial state.
virtual void EventAttributes(const EventSet &rEventSet)
Set attributes for existing events.
void InsInitStates(const StateSet &rStates)
Add (perhaps new) anonymous initial states to generator
bool StateNamesEnabled(void) const
Whether libFAUEDS functions are requested to generate state names.
StateSet::Iterator InitStatesEnd(void) const
Iterator to End() of mInitStates.
Idx TransRelSize(void) const
Get number of transitions.
Idx Size(void) const
Get generator size (number of states)
bool ExistsInitState(Idx index) const
Test existence of state in mInitStates.
std::string SStr(Idx index) const
Return pretty printable state name for index (eg for debugging)
bool ExistsMarkedState(Idx index) const
Test existence of state in mMarkedStates.
void InjectAlphabet(const EventSet &rNewalphabet)
Set mpAlphabet without consistency check.
virtual const AttributeVoid * AttributeType(void) const
Attribute typeinfo.
Definition: cfl_baseset.h:2171
bool Empty(void) const
Test whether if the TBaseSet is Empty.
Definition: cfl_baseset.h:1824
bool Exists(const T &rElem) const
Test existence of element.
Definition: cfl_baseset.h:2115
virtual void Clear(void)
Clear all set.
Definition: cfl_baseset.h:1902
virtual bool AttributeTest(const Type &rAttr) const
Attribute typeinfo.
Definition: cfl_baseset.h:2177
Iterator End(void) const
Iterator to the end of set.
Definition: cfl_baseset.h:1896
virtual void InsertSet(const TBaseSet &rOtherSet)
Insert elements given by rOtherSet.
Definition: cfl_baseset.h:1987
Iterator Begin(void) const
Iterator to the begin of set.
Definition: cfl_baseset.h:1891
virtual const AttributeVoid & Attribute(const T &rElem) const
Attribute access.
Definition: cfl_baseset.h:2290
virtual bool Erase(const T &rElem)
Erase element by reference.
Definition: cfl_baseset.h:2019
Idx Size(void) const
Get Size of TBaseSet.
Definition: cfl_baseset.h:1819
void StateMin(const Generator &rGen, Generator &rResGen)
State set minimization.
void ProjectNonDetScc(Generator &rGen, const EventSet &rProjectAlphabet)
Language projection.
void aProjectNonDet(Generator &rGen, const EventSet &rProjectAlphabet)
Language projection.
bool ComputeScc(const Generator &rGen, const SccFilter &rFilter, std::list< StateSet > &rSccList, StateSet &rRoots)
Compute strongly connected components (SCC)
void Deterministic(const Generator &rGen, Generator &rResGen)
Make generator deterministic.
void aInvProject(Generator &rGen, const EventSet &rProjectAlphabet)
Inverse projection.
void ProjectNonDet(Generator &rGen, const EventSet &rProjectAlphabet)
Language projection.
void Project(const Generator &rGen, const EventSet &rProjectAlphabet, Generator &rResGen)
Deterministic projection.
void InvProject(Generator &rGen, const EventSet &rProjectAlphabet)
Inverse projection.
void aProject(const Generator &rGen, const EventSet &rProjectAlphabet, Generator &rResGen)
Deterministic projection.
libFAUDES resides within the namespace faudes.
uint32_t Idx
Type definition for index type (allways 32bit)
void LoopCallback(bool pBreak(void))
Definition: cfl_helper.cpp:621
void ProjectNonDet_fbr(Generator &rGen, const EventSet &rProjectAlphabet)
TGraph< Idx, Idx > Graph
void ProjectNonDet_ref(Generator &rGen, const EventSet &rProjectAlphabet)
void CreateEntryStatesMap(const std::map< StateSet, Idx > &rRevEntryStatesMap, std::map< Idx, StateSet > &rEntryStatesMap)
std::string CollapsString(const std::string &rString, unsigned int len)
Limit length of string, return head and tail of string.
Definition: cfl_helper.cpp:91
void ProjectNonDet_scc(Generator &rGen, const EventSet &rProjectAlphabet)
TNode< Idx, Idx > Node
void LocalAccessibleReach(const Generator &rLowGen, const EventSet &rHighAlph, Idx lowState, StateSet &rAccessibleReach)
Compute the accessible reach for a local automaton.
void ProjectNonDet_simple(Generator &rGen, const EventSet &rProjectAlphabet)
void ProjectNonDet_graph(Generator &rGen, const EventSet &rProjectAlphabet)
void ProjectNonDet_opitz(Generator &rGen, const EventSet &rProjectAlphabet)
Definition: cfl_project.cpp:46
void ProjectNonDet_barthel(Generator &rGen, const EventSet &rProjectAlphabet)
long int Int
Type definition for integer type (let target system decide, minimum 32bit)
Specialisation of the graph template to provide convenience methods addressing the intended ussage.
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)
Iterator End(void) const
void Import(vGenerator &rGen)
void Erase(Iterator git, TNode< Idx, Idx >::Iterator nit)
Graph data structure for transitionrelation – EXPERIMENTAL.
graph_iterator_t< VLabel, ELabel > Iterator
static Iterator InfX1(void)
A node represents the edges related to one individual vertex.
node_iterator_t< VLabel, ELabel > Iterator
TNode(const typename std::set< node_entry_t< VLabel, ELabel > > n)
An iterator over the map of all nodes is interpreted as a state incl.
graph_iterator_t(typename TGraph< VLabel, ELabel >::iterator git)
graph_iterator_t< VLabel, ELabel > * FakeConst(void) const
Int UsrFlg(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
VLabel X1(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
A node-entry represents one edge.
node_entry_t(void)
graph_iterator_t< VLabel, ELabel > X2It
node_entry_t(ELabel ev, graph_iterator_t< VLabel, ELabel > x2it)
ELabel Ev
bool operator<(const node_entry_t< VLabel, ELabel > &ent) const
node_entry_t(const node_entry_t< VLabel, ELabel > &ent)
An iterator over the set of edges related to one vertex is interpreted as a transition.
ELabel Ev(void) const
graph_iterator_t< VLabel, ELabel > X2It(void) const
VLabel X2(void) const
node_iterator_t(const typename TNode< VLabel, ELabel >::iterator &nit)

libFAUDES 2.32b --- 2024.03.01 --- c++ api documentaion by doxygen