mtc_project.cpp
Go to the documentation of this file.
1 /** @file mtc_project.cpp
2 
3 Methods for computing the natural projection of multitasking generators
4 
5 */
6 
7 /* FAU Discrete Event Systems Library (libfaudes)
8 
9  Copyright (C) 2008 Matthias Singer
10  Copyright (C) 2006 Bernd Opitz
11  Exclusive copyright is granted to Klaus Schmidt
12 
13  This library is free software; you can redistribute it and/or
14  modify it under the terms of the GNU Lesser General Public
15  License as published by the Free Software Foundation; either
16  version 2.1 of the License, or (at your option) any later version.
17 
18  This library is distributed in the hope that it will be useful,
19  but WITHOUT ANY WARRANTY; without even the implied warranty of
20  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
21  Lesser General Public License for more details.
22 
23  You should have received a copy of the GNU Lesser General Public
24  License along with this library; if not, write to the Free Software
25  Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA */
26 
27 
28 #include "mtc_project.h"
29 #include "cfl_localgen.h"
30 
31 namespace faudes {
32 
33 // mtcUniqueInit(rGen&)
34 void mtcUniqueInit(MtcSystem& rGen) {
35  Idx inituni;
36  StateSet::Iterator lit;
38  // check number of initial states
39  if (rGen.InitStatesSize() <= 1) return;
40  // introduce new initial state
41  if (rGen.StateNamesEnabled()) {
42  std::string initname=rGen.UniqueStateName("InitUni");
43  inituni = rGen.InsState(initname);
44  }
45  else {
46  inituni = rGen.InsState();
47  }
48  FD_DF("mtcUniqueInit: introducing new initial state: " << inituni);
49  // introduce outgoing transitions from initial state
50  FD_DF("mtcUniqueInit: introduce outgoing transitions: ");
51  for (lit = rGen.InitStatesBegin(); lit != rGen.InitStatesEnd(); ++lit) {
52  for (tit = rGen.TransRelBegin(*lit); tit != rGen.TransRelEnd(*lit); ++tit) {
53  rGen.SetTransition(inituni, tit->Ev, tit->X2);
54  FD_DF("mtcUniqueInit: " << inituni << "-" << tit->Ev << "-" << tit->X2);
55  }
56  // colored states
57  const ColorSet& colors = rGen.Colors(*lit);
58  rGen.InsColors(inituni, colors);
59  // marked states
60  if (!rGen.MarkedStatesEmpty()) {
61  rGen.SetMarkedState(inituni);
62  FD_DF("mtcUniqueInit: set marked state: " << inituni);
63  }
64  }
65  // delete old istates
66  rGen.ClearInitStates();
67  // set inituni as new initial state
68  rGen.SetInitState(inituni);
69 }
70 
71 
72 // mtcDeterministic(rGen&, rResGen&)
73 void mtcDeterministic(const MtcSystem& rGen, MtcSystem& rResGen) {
74  // temporary vectors
75  std::vector<StateSet> power_states;
76  std::vector<Idx> det_states;
77  mtcDeterministic(rGen, power_states, det_states, rResGen);
78 }
79 
80 
81 // mtcDeterministic(rGen&, rEntryStatesMap&, rResGen&)
82 void mtcDeterministic(const MtcSystem& rGen, std::map<Idx,StateSet>& rEntryStatesMap,
83  MtcSystem& rResGen) {
84  // prepare result:
85  rEntryStatesMap.clear();
86  // helpers:
87  std::vector<StateSet> power_states;
88  std::vector<Idx> det_states;
89  // call Deterministic function
90  mtcDeterministic(rGen, power_states, det_states, rResGen);
91  // build entry states map
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]));
95  }
96 }
97 
98 
99 void mtcDeterministic(const MtcSystem& rGen, std::vector<StateSet>& rPowerStates,
100  std::vector<Idx>& rDetStates, MtcSystem& rResGen) {
101  // set the name
102  rResGen.Name("Det(" + rGen.Name() + ")");
103 
104  // prepare result
105  rPowerStates.clear();
106  rDetStates.clear();
107  rResGen.Clear();
108 
109  // copy alphabet
110  rResGen.InjectAlphabet(rGen.Alphabet());
111 
112  // helpers
113  TransSetEvX1X2 trel_evx1x2;
114  rGen.TransRel(trel_evx1x2);
115  typedef std::multimap< Idx,std::vector<StateSet>::size_type > T_HASHMAP;
116  T_HASHMAP hashmap;
117  std::vector<StateSet>::size_type current_vecindex;
118  std::pair< std::map<StateSet,Idx>::iterator,bool > result;
119  TransSet::Iterator transrel_end = rGen.TransRelEnd();
120  StateSet newset;
121  StateSet::Iterator lit;
122  const Idx max_idx = std::numeric_limits<Idx>::max();
123  if (rGen.InitStatesEmpty()) {
124  return;
125  }
126 // std::map<Idx,ColorSet> CopyMap = rGen.StateColorMap();
127  Idx newstate = rResGen.InsInitState();
128  // initialize rPowerStates with subset of initial states
129  for (lit = rGen.InitStatesBegin(); lit != rGen.InitStatesEnd(); ++lit) {
130  // clear set and insert single state
131  newset.Insert(*lit);
132  const ColorSet& colors = rGen.Colors(*lit);
133  // set colored state if a member state is colored
134  rResGen.InsColors(newstate,colors);
135  }
136  FD_DF("mtcDeterministic: created subset of initial states {"
137  << newset.ToString() << "} with deterministic state index " << rGen.SStr(newstate));
138  // insert newset in rPowerStates
139  rPowerStates.push_back(newset);
140  rDetStates.push_back(newstate);
141  hashmap.insert(std::make_pair(newset.Signature(), (Idx)rPowerStates.size() - 1));
142 
143  // iteration over all states
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]);
147 
148  std::vector<StateSet> newset_vec;
149  std::vector<Idx> event_vec;
150 
151  // multiway merge begin
152  FD_DF("mtcDeterministic: starting multiway merge...");
153  std::list<TransSet::Iterator> merge_iterators;
154  std::vector<Transition> trans_vec;
155 
156  // add transset iterator at begin of each state's transitions
157  TransSet::Iterator tit;
158  for (lit = rPowerStates[current_vecindex].Begin();
159  lit != rPowerStates[current_vecindex].End(); ++lit) {
160  tit = rGen.TransRelBegin(*lit);
161  if (tit != rGen.TransRelEnd(*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));
165  }
166  }
167 
168  // find first iterator with lowest event
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;
176  currentit = i;
177  }
178  }
179  // currentit now holds the iterator
180  // currentevent holds the lowest event (lowest Idx)
181 
182  // merge all transitions with currentevent at each iterator in a row
183  // this is a modification of multiway merge as after projection the
184  // automaton most likely holds states with many transitions that share
185  // the same event. only merging the lowest transition and continue with
186  // search for the lowest event again would be to slow here (because
187  // of too much iterator dereferencing).
188  Idx currentstate;
189  while (currentit != merge_iterators.end()) {
190  currentstate = (*currentit)->X1;
191  TransSet::Iterator& j = *currentit;
192  while (1) {
193  // remove iterator if it reaches the end of the transition set
194  if (j == transrel_end) {
195  std::list<TransSet::Iterator>::iterator tmpit = currentit;
196  ++currentit;
197  merge_iterators.erase(tmpit);
198  break;
199  }
200  // if current iterator is in its original state
201  else if (j->X1 == currentstate) {
202  // if the event is still the same add the transition
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));
207  }
208  // else go to next iterator
209  else {
210  ++currentit;
211  break;
212  }
213  }
214  // if the iterator is beyond its original state remove it
215  else {
216  std::list<TransSet::Iterator>::iterator tmpit = currentit;
217  ++currentit;
218  merge_iterators.erase(tmpit);
219  break;
220  }
221  ++j;
222  }
223  }
224  }
225 
226  // partition transition vector by events. optimizable?
227  FD_DF("mtcDeterministic: partitioning the transition vector...");
228  std::vector<Transition>::iterator tv_it;
229  StateSet newset;
230  Idx lastevent = 0;
231  for (tv_it = trans_vec.begin(); tv_it != trans_vec.end(); ++tv_it) {
232  if ((tv_it->Ev == lastevent) || (lastevent == 0)) {
233  newset.Insert(tv_it->X2);
234  lastevent = tv_it->Ev;
235  }
236  else {
237  FD_DF("mtcDeterministic: partition: {" << newset.ToString()
238  << "} with event " << rGen.EStr(lastevent));
239  newset_vec.push_back(newset);
240  event_vec.push_back(lastevent);
241  newset.Clear();
242  newset.Insert(tv_it->X2);
243  lastevent = tv_it->Ev;
244  }
245  }
246  if (! newset.Empty()) {
247  FD_DF("mtcDeterministic: partition: {" << newset.ToString()
248  << "} with event " << rGen.EStr(lastevent));
249  newset_vec.push_back(newset);
250  event_vec.push_back(lastevent);
251  }
252  FD_DF("mtcDeterministic: partitioning the transition vector finished");
253  FD_DF("mtcDeterministic: multiway merge finished");
254  // multiway merge end
255 
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];
260  Idx tmp_x2 = 0;
261  Idx sig = currentset.Signature();
262  // test if newset signature is already known
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) {
267  // test set of every matching signature for equality
268  if (currentset == rPowerStates[hit->second]) {
269  tmp_x2 = rDetStates[hit->second];
270  break;
271  }
272  }
273 
274  // if new set is unique within the existing power sets
275  if (tmp_x2 == 0) {
276  // create new state in res generator
277  tmp_x2 = rResGen.InsState();
278  // insert newset in rPowerStates and get iterator,bool pair
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() << "}");
284  // set colored if one of the states in current set is colored
285  for (lit = currentset.Begin(); lit != currentset.End(); ++lit) {
286  const ColorSet& colors = rGen.Colors(*lit);
287  rResGen.InsColors(tmp_x2,colors);
288  FD_DF("mtcDeterministic: setting as colored: " << rGen.SStr(tmp_x2));
289  }
290  }
291  // introduce transition
292  rResGen.SetTransition(rDetStates[current_vecindex], currentevent, tmp_x2);
293  }
294  }
295  // fix names
296  if (rGen.StateNamesEnabled() && rResGen.StateNamesEnabled()) {
297  FD_DF("mtcDeterministic: fixing names...");
298  // rPowerStates / rDetStates index "iterator"
299  std::vector<StateSet>::size_type i;
300  // deterministic states iterator
301  std::vector<Idx>::const_iterator dit;
302  for (i = 0; i < rPowerStates.size(); ++i) {
303  // temporary state name
304  std::string name = "{";
305  for (lit = rPowerStates[i].Begin(); lit != rPowerStates[i].End(); ++lit) {
306  if (rResGen.StateName(*lit) != "") {
307  name = name + rResGen.StateName(*lit) + ",";
308  }
309  else {
310  name = name + ToStringInteger(*lit) + ",";
311  }
312  }
313  name.erase(name.length() - 1);
314  name = name + "}";
315  rResGen.StateName(rDetStates[i], name);
316  FD_DF("mtcDeterministic: setting state name \"" << name << "\" for index " << rDetStates[i]);
317  }
318  }
319  // Delete unnecessary events and set event attributes
320  rResGen.DelEvents(rResGen.UnusedEvents());
321  EventSet usedEvents = rResGen.UsedEvents();
322  rResGen.SetControllable(rGen.ControllableEvents()*usedEvents);
323  rResGen.SetForcible(rGen.ForcibleEvents()*usedEvents);
324  rResGen.ClrObservable(rGen.UnobservableEvents()*usedEvents);
325 }
326 
327 // mtcProjectNonDet(rGen&, rProjectAlphabet&)
328 void mtcProjectNonDet(MtcSystem& rGen, const EventSet& rProjectAlphabet) {
329 
330  // HELPERS:
331  StateSet reach; // StateSet for reachable states
332  std::stack<Idx> todo; // todo stack
333  StateSet done; // done set
334  Idx currentstate; // the currently processed state
335  StateSet::Iterator lit;
336  TransSet::Iterator tit;
337  TransSet::Iterator tit_end;
338 
339  // ALGORITHM:
340  // initialize algorithm by pushing init states on todo stack
341  for (lit = rGen.InitStatesBegin(); lit != rGen.InitStatesEnd(); ++lit) {
342  FD_DF("mtcProjectNonDet: todo add: " << rGen.SStr(*lit));
343  todo.push(*lit);
344  }
345 
346  // process todo stack
347  while (! todo.empty()) {
348  currentstate = todo.top();
349  todo.pop();
350  done.Insert(currentstate); // mark as done
351  FD_DF("mtcProjectNonDet: current state: " << rGen.SStr(currentstate));
352 
353  // comp accessible reach
354  reach.Clear();
355  LocalAccessibleReach(rGen, rProjectAlphabet, currentstate, reach);
356  FD_DF("mtcProjectNonDet: local reach: " << reach.ToString());
357 
358  // remove all transitions that leave current state
359  // with an invisible event
360  tit = rGen.TransRelBegin(currentstate);
361  tit_end = rGen.TransRelEnd(currentstate);
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");
367  TransSet::Iterator tit_tmp = tit;
368  ++tit;
369  rGen.ClrTransition(tit_tmp);
370  }
371  else {
372  ++tit;
373  }
374  }
375 
376  // relink outgoing transitions
377  FD_DF("mtcProjectNonDet: relinking outgoing transitions...");
378  for (lit = reach.Begin(); lit != reach.End(); ++lit) {
379  tit = rGen.TransRelBegin(*lit);
380  tit_end = rGen.TransRelEnd(*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));
384  rGen.SetTransition(currentstate, tit->Ev, tit->X2);
385  if (! done.Exists(tit->X2)) {
386  FD_DF("mtcProjectNonDet: todo push: " << rGen.SStr(tit->X2));
387  todo.push(tit->X2);
388  }
389  }
390  }
391  // colored status test
392  const ColorSet& colors = rGen.Colors(*lit);
393  if (!colors.Empty()) {
394  FD_DF("mtcProjectNonDet: setting colored state " << rGen.SStr(currentstate));
395  rGen.InsColors(currentstate, colors);
396  }
397  }
398  }
399 
400  // inject projection alphabet
401  rGen.InjectAlphabet(rProjectAlphabet);
402 
403  EventSet unused = rGen.UnusedEvents();
404  EventSet::Iterator eit;
405  for(eit = unused.Begin(); eit != unused.End(); ++eit){
406  rGen.ClrEventAttribute(*eit);
407  rGen.EventSymbolTablep()->ClrEntry(*eit);
408  rGen.DelEvent(*eit);
409  }
410  // set name
411  rGen.Name("MtcPro(" + rGen.Name() + ")" );
412 }
413 
414 // wrapper
415 void mtcProjectNonDet(const MtcSystem& rGen, const EventSet& rProjectAlphabet, MtcSystem& rResGen) {
416  rResGen=rGen;
417  mtcProjectNonDet(rResGen,rProjectAlphabet);
418 }
419 
420 // mtcProject(rGen, rProjectAlphabet, rResGen&)
421 void mtcProject(const MtcSystem& rGen, const EventSet& rProjectAlphabet, MtcSystem& rResGen) {
422  // algorithm:
423  // temporary copy of rGen
424  MtcSystem tmp;
425  // temporarily assign rGen to rResGen
426  MtcSystem copyGen = MtcSystem(rGen);
427  // project rResGen with respect to rProjectAlphabet
428  mtcProjectNonDet(copyGen, rProjectAlphabet);
429 #ifdef FAUDES_DEBUG_FUNCTION
430  FD_WARN("mtcProject: debug out")
431  copyGen.Write("tmp_project_nd.gen");
432 #endif
433  // put deterministic result into tmp
434  mtcDeterministic(copyGen, tmp);
435 #ifdef FAUDES_DEBUG_FUNCTION
436  FD_WARN("mtcProject: debug out")
437  tmp.Write("tmp_project_d.gen");
438 #endif
439  // minimize states and rewrite result to rResGen
440  mtcStateMin(tmp, rResGen);
441 #ifdef FAUDES_DEBUG_FUNCTION
442  FD_WARN("mtcProject: debug out")
443  rResGen.Write("tmp_project_m.gen");
444 #endif
445  // set controllability status TODO: other event attributes
446  rResGen.SetControllable(rGen.ControllableEvents()*rProjectAlphabet);
447  // set name
448  rResGen.Name(rResGen.Name()+": mtcProject");
449 }
450 
451 
452 // mtcProject(rGen, rProjectAlphabet, rEntryStatesMap&, rResGen&)
453 void mtcProject(const MtcSystem& rGen, const EventSet& rProjectAlphabet,
454  std::map<Idx,StateSet>& rEntryStatesMap, MtcSystem& rResGen) {
455  // temporary copy of rGen
456  MtcSystem tmp;
457  MtcSystem copyGen = MtcSystem(rGen);
458  // temporary entry state map
459  std::map<Idx,StateSet> tmp_entrystatemap;
460  // temporarily assign rGen to rResGen
461  // std::cout << " copied low-level generator " << std::endl;
462  // copyGen.DWrite();
463  // project tmp with respect to palphabet
464  mtcProjectNonDet(copyGen, rProjectAlphabet);
465 
466  // put deterministic result into tmp
467  mtcDeterministic(copyGen, tmp_entrystatemap, tmp);
468  // write entry state map for minimized generator
469  std::vector<StateSet> subsets;
470  std::vector<Idx> newindices;
471  // minimize states and rewrite result to rResGen
472  mtcStateMin(tmp, rResGen, subsets, newindices);
473  // rResGen.DWrite();
474  // build entry state map
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) {
479  StateSet tmpstates;
480  for (sit = subsets[i].Begin(); sit != subsets[i].End(); ++sit) {
481  esmit = tmp_entrystatemap.find(*sit);
482 #ifdef FD_CHECKED
483  if (esmit == tmp_entrystatemap.end()) {
484  FD_WARN("mtcproject internal error");
485  abort();
486  }
487 #endif
488  // insert entry states in temporary StateSet
489  tmpstates.InsertSet(esmit->second);
490  }
491 
492  rEntryStatesMap.insert(std::make_pair(newindices[i], tmpstates));
493  }
494 }
495 
496 
497 // mtcInvProject(rGen&, rProjectAlphabet)
498 void mtcInvProject(MtcSystem& rGen, const EventSet& rProjectAlphabet) {
499  // test if the alphabet of the generator is included in the given alphabet
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);
504  }
505  EventSet newevents = rProjectAlphabet - rGen.Alphabet();
506  // insert events into generator
507  rGen.InsEvents(newevents);
508  FD_DF("mtcInvProject: adding events \"" << newevents.ToString() << "\" at every state");
509  StateSet::Iterator lit;
510  EventSet::Iterator eit;
511  for (lit = rGen.StatesBegin(); lit != rGen.StatesEnd(); ++lit) {
512  for (eit = newevents.Begin(); eit != newevents.End(); ++eit)
513  rGen.SetTransition(*lit, *eit, *lit);
514  }
515 }
516 
517 // RTI wrapper
518 void mtcInvProject(const MtcSystem& rGen, const EventSet& rProjectAlphabet, MtcSystem& rResGen) {
519  rResGen=rGen;
520  mtcInvProject(rResGen,rProjectAlphabet);
521 }
522 
523 } // namespace faudes
#define FD_WARN(message)
#define FD_DF(message)
Idx Signature(void) const
bool Exists(const Idx &rIndex) const
void ClrEntry(Idx index)
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Definition: cfl_transset.h:273
virtual void Clear(void)
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
Definition: cfl_types.cpp:170
void Write(const Type *pContext=0) const
Definition: cfl_types.cpp:140
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
bool DelEvent(Idx index)
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
void Name(const std::string &rName)
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 Empty(void) const
Definition: cfl_baseset.h:1841
bool Exists(const T &rElem) const
Definition: cfl_baseset.h:2132
virtual void Clear(void)
Definition: cfl_baseset.h:1919
Iterator End(void) const
Definition: cfl_baseset.h:1913
virtual void InsertSet(const TBaseSet &rOtherSet)
Definition: cfl_baseset.h:2004
Iterator Begin(void) const
Definition: cfl_baseset.h:1908
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)
Definition: mtc_project.cpp:73
uint32_t Idx
void mtcStateMin(MtcSystem &rGen, MtcSystem &rResGen)
void mtcUniqueInit(MtcSystem &rGen)
Definition: mtc_project.cpp:34
TmtcGenerator< AttributeVoid, AttributeColoredState, AttributeCFlags, AttributeVoid > MtcSystem
void LocalAccessibleReach(const Generator &rLowGen, const EventSet &rHighAlph, Idx lowState, StateSet &rAccessibleReach)
std::string ToStringInteger(Int number)
Definition: cfl_utils.cpp:43

libFAUDES 2.33b --- 2025.05.07 --- c++ api documentaion by doxygen