syn_supcon.cpp
Go to the documentation of this file.
1 /** @file syn_supcon.cpp Supremal controllable sublanguage */
2 
3 /* FAU Discrete Event Systems Library (libfaudes)
4 
5  Copyright (C) 2006 Bernd Opitz
6  Exclusive copyright is granted to Klaus Schmidt
7 
8  This library is free software; you can redistribute it and/or
9  modify it under the terms of the GNU Lesser General Public
10  License as published by the Free Software Foundation; either
11  version 2.1 of the License, or (at your option) any later version.
12 
13  This library is distributed in the hope that it will be useful,
14  but WITHOUT ANY WARRANTY; without even the implied warranty of
15  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
16  Lesser General Public License for more details.
17 
18  You should have received a copy of the GNU Lesser General Public
19  License along with this library; if not, write to the Free Software
20  Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA */
21 
22 
23 #include "syn_supcon.h"
24 
25 
26 namespace faudes {
27 
28 
29 
30 
31 /*
32 ***************************************************************************************
33 ***************************************************************************************
34  Implementation
35 ***************************************************************************************
36 ***************************************************************************************
37 */
38 
39 
40 /*
41 Revision fro libFAUDES 2.20b:
42 
43 SupCon and IsControllable used to share the same algorithm to identify critical
44 states, implemented as IsControllableUnchecked().
45 
46 The implementation, however, was only correct under the assumption that the state set of the
47 supervisor/candidate H would also distinguish plant states. The later assumption is
48 true in the context of SupCon, where the candidate is build as the parallel composition.
49 It is not true in general.
50 
51 Thus, in libFAUDES 2.20b the original algorithm was moved from IsControllableUnchecked to
52 SupConClosedUnchecked and IsControllableUnchecked was reimplemented.
53 */
54 
55 
56 // SupConClosedUnchecked(rPlantGen, rCAlph, rSupCandGen)
57 void SupConClosedUnchecked(
58  const Generator& rPlantGen, // aka G
59  const EventSet& rCAlph,
60  Generator& rSupCandGen // aka H
61 )
62 {
63  FD_DF("SupConClosedUnchecked(" << &rSupCandGen << "," << &rPlantGen << ")");
64 
65  // bail out if plant or candidate contain no initial states
66  if(rPlantGen.InitStatesEmpty() || rSupCandGen.InitStatesEmpty())
67  return;
68 
69  // todo stack (pairs of states)
70  std::stack<Idx> todog, todoh;
71  // set of already processed states of H (this is where we need H-states to also distinguish G-states)
72  StateSet processed;
73  // reverse sorted transition relation of H (to be built on the fly)
74  TransSetX2EvX1 rtransrel;
75  // critical states
76  StateSet critical;
77 
78  // push combined initial state on todo stack
79  todog.push(*rPlantGen.InitStatesBegin());
80  todoh.push(*rSupCandGen.InitStatesBegin());
81  FD_DF("SupCon: todo push: (" << rPlantGen.SStr(*rPlantGen.InitStatesBegin()) << "|"
82  << rSupCandGen.SStr(*rSupCandGen.InitStatesBegin()) << ")");
83 
84  // process todo stack
85  while (! todog.empty()) {
86  // allow for user interrupt
87  // LoopCallback();
88  // allow for user interrupt, incl progress report
89  FD_WPC(1,2,"Controllability(): iterating states");
90  // get top element from todo stack
91  Idx currentg = todog.top();
92  Idx currenth = todoh.top();
93  todog.pop();
94  todoh.pop();
95  FD_DF("SupCon: todo pop: (" << rPlantGen.SStr(currentg) << "|"
96  << rSupCandGen.SStr(currenth) << ")");
97 
98  // break on doublets (tmoor 201104)
99  if(processed.Exists(currenth)) continue;
100 
101 #ifdef FAUDES_DEBUG_FUNCTION
102  TransSet::Iterator _titg, _tith;
103  // print all transitions of current states
104  FD_DF("SupCon: transitions from current states:");
105  for (_titg = rPlantGen.TransRelBegin(currentg); _titg != rPlantGen.TransRelEnd(currentg); ++_titg)
106  FD_DF("SupCon: g: " << rPlantGen.SStr(_titg->X1) << "-"
107  << rPlantGen.EStr(_titg->Ev) << "-" << rPlantGen.SStr(_titg->X2));
108  for (_tith = rSupCandGen.TransRelBegin(currenth); _tith != rSupCandGen.TransRelEnd(currenth); ++_tith)
109  FD_DF("SupCon: h: " << rSupCandGen.SStr(_tith->X1) << "-"
110  << rSupCandGen.EStr(_tith->Ev) << "-" << rSupCandGen.SStr(_tith->X2));
111 #endif
112 
113  // process all h transitions while there could be matching g transitions
114  TransSet::Iterator titg = rPlantGen.TransRelBegin(currentg);
115  TransSet::Iterator titg_end = rPlantGen.TransRelEnd(currentg);
116  TransSet::Iterator tith = rSupCandGen.TransRelBegin(currenth);
117  TransSet::Iterator tith_end = rSupCandGen.TransRelEnd(currenth);
118  while ((tith != tith_end) && (titg != titg_end)) {
119  FD_DF("SupCon: processing g-transition: " << rPlantGen.SStr(titg->X1)
120  << "-" << rPlantGen.EStr(titg->Ev) << "-" << rPlantGen.SStr(titg->X2));
121  FD_DF("SupCon: processing h-transition: " << rSupCandGen.SStr(tith->X1)
122  << "-" << rSupCandGen.EStr(tith->Ev) << "-" << rSupCandGen.SStr(tith->X2));
123  // increment tith and titg case A: process common events
124  if (titg->Ev == tith->Ev) {
125  FD_DF("SupCon: processing common event " << rPlantGen.EStr(titg->Ev));
126  // add to todo list if state not processed (tmoor 201104: record next H state on stack)
127  if(!processed.Exists(tith->X2)) {
128  todog.push(titg->X2);
129  todoh.push(tith->X2);
130  FD_DF("SupCon: todo push: (" << rPlantGen.SStr(titg->X2) << "|"
131  << rSupCandGen.SStr(tith->X2) << ")");
132  }
133  // if h successor state is not critical add transition to rtransrel
134  if (!critical.Exists(tith->X2)) {
135  rtransrel.Insert(*tith);
136  FD_DF("SupCon: incrementing g and h transrel");
137  ++titg;
138  ++tith;
139  }
140  // if successor state is critical and event uncontrollable
141  else if (!rCAlph.Exists(titg->Ev)) {
142  FD_DF("SupCon: successor state " << rSupCandGen.SStr(tith->X2) <<
143  " critical and event " << rPlantGen.EStr(titg->Ev) << " uncontrollable:");
144  FD_DF("SupCon: TraverseUncontrollableBackwards(" << rSupCandGen.SStr(currenth) << ")");
145  TraverseUncontrollableBackwards(rCAlph, rtransrel, critical, currenth);
146 #ifdef FAUDES_CHECKED
147  // just increment transrel iterators to find all h transitions not in g
148  FD_DF("IsControllable: incrementing g an h transrel (FAUDES_CHECKED)");
149  ++titg;
150  ++tith;
151  break;
152 #else
153  // exit all loops
154  titg = titg_end;
155  tith = tith_end;
156  break;
157 #endif
158  }
159  // if successor state is critical and event controllable
160  else {
161  FD_DF("SupCon: incrementing g and h transrel");
162  ++titg;
163  ++tith;
164  }
165  }
166  // increment tith and titg case B: process g event that is not enabled in h
167  else if (titg->Ev < tith->Ev) {
168  FD_DF("SupCon: asynchronous execution of event "
169  << rPlantGen.EStr(titg->Ev) << " in g while " << rSupCandGen.EStr(tith->Ev)
170  << " in h");
171  // if uncontrollable transition violates specification
172  // delete state from rResGen and put into criticalset
173  if (!rCAlph.Exists(titg->Ev)) {
174  FD_DF("SupCon: asynchronous event " << rPlantGen.EStr(titg->Ev)
175  << " in g is uncontrollable");
176  FD_DF("SupCon: TraverseUncontrollableBackwards(" << rSupCandGen.SStr(currenth) << ")");
177  TraverseUncontrollableBackwards(rCAlph, rtransrel, critical, currenth);
178  // exit all loops over g transrel
179  titg = titg_end;
180  break;
181  }
182  FD_DF("SupCon: incrementing g transrel");
183  ++titg;
184  }
185  // increment tith and titg case C: process h event that is not enabled in g
186  else {
187  // #ifdef FAUDES_CHECKED
188  // FD_WARN("SupCon: transition " << rSupCandGen.TStr(*tith)
189  // << " in specification h not found in g");
190  // #endif
191  FD_DF("SupCon: incrementing h transrel");
192  ++tith;
193  }
194  } // end while tith and titg
195  // increment tith and titg case D: process leftover g events
196  while (titg != titg_end) {
197  FD_DF("SupCon: asynchronous execution of event "
198  << rPlantGen.EStr(titg->Ev) << " in g at end of h");
199  FD_DF("SupCon: actual g-transition: " << rPlantGen.SStr(titg->X1)
200  << "-" << rPlantGen.EStr(titg->Ev) << "-" << rPlantGen.SStr(titg->X2));
201  FD_DF("SupCon: actual h-transition: end");
202  // if uncontrollable transition violates specification
203  if (!rCAlph.Exists(titg->Ev)) {
204  FD_DF("SupCon: asynchronous execution of uncontrollable event "
205  << rPlantGen.EStr(titg->Ev) << " in g");
206  FD_DF("SupCon: TraverseUncontrollableBackwards(" << rPlantGen.SStr(currenth) << ")");
207  TraverseUncontrollableBackwards(rCAlph, rtransrel, critical, currenth);
208  // exit this loop
209  break;
210  }
211  FD_DF("SupCon: incrementing g transrel");
212  ++titg;
213  }
214  //#ifdef FAUDES_CHECKED
215  // increment tith and titg case E: process leftover h events
216  //while (tith != tith_end) {
217  // FD_WARN("SupCon: transition " << rSupCandGen.TStr(*tith) << " in specification h not found in g");
218  // FD_DF("SupCon: incrementing h transrel");
219  // ++tith;
220  //}
221  //#endif
222  processed.Insert(currenth);
223  } //end while todog
224 
225  // remove all states that have been identified as critical or that have
226  // been not processed
227  critical = rSupCandGen.States() - ( processed - critical );
228  rSupCandGen.DelStates(critical);
229 }
230 
231 
232 
233 /*
234 Revision for libFAUDES 2.20b:
235 
236 The re-implemented version will only report states as critical
237 if they disable an uncontrollable plant event. No reverse
238 search is performed.
239 */
240 
241 
242 // IsControllableUnchecked(rPlantGen, rCAlph, rSupCandGen, rCriticalStates)
243 bool IsControllableUnchecked(
244  const Generator& rPlantGen,
245  const EventSet& rCAlph,
246  const Generator& rSupCandGen,
247  StateSet& rCriticalStates)
248 {
249  FD_DF("IsControllableUnchecked(" << &rSupCandGen << "," << &rPlantGen << ")");
250 
251  // todo stack
252  std::stack< std::pair<Idx,Idx> > todo;
253  // set of already processed states
254  std::set< std::pair<Idx,Idx> > processed;
255 
256  // PREPARE RESULT:
257  rCriticalStates.Clear();
258  rCriticalStates.Name("CriticalStates");
259 
260  // return true (controllable) if there is no initial state
261  if(rPlantGen.InitStatesEmpty() || rSupCandGen.InitStatesEmpty())
262  return true;
263 
264  // push combined initial state on todo stack
265  todo.push( std::make_pair(*rPlantGen.InitStatesBegin(),*rSupCandGen.InitStatesBegin()) );
266  FD_DF("IsControllable: todo push: (" << rPlantGen.SStr(*rPlantGen.InitStatesBegin()) << "|"
267  << rSupCandGen.SStr(*rSupCandGen.InitStatesBegin()) << ")");
268 
269  // process todo stack
270  while (! todo.empty()) {
271  // allow for user interrupt
272  // LoopCallback();
273  // allow for user interrupt, incl progress report
274  FD_WPC(1,2,"Controllability(): iterating states");
275  // get top element from todo stack
276  std::pair<Idx,Idx> current = todo.top(); todo.pop();
277  processed.insert(current);
278  Idx currentg = current.first;
279  Idx currenth = current.second;
280  FD_DF("IsControllable: todo pop: (" << rPlantGen.SStr(currentg) << "|"
281  << rSupCandGen.SStr(currenth) << ")");
282 
283 #ifdef FAUDES_DEBUG_FUNCTION
284  TransSet::Iterator _titg, _tith;
285  // print all transitions of current states
286  FD_DF("IsControllable: transitions from current states:");
287  for (_titg = rPlantGen.TransRelBegin(currentg); _titg != rPlantGen.TransRelEnd(currentg); ++_titg)
288  FD_DF("IsControllable: g: " << rPlantGen.SStr(_titg->X1) << "-"
289  << rPlantGen.EStr(_titg->Ev) << "-" << rPlantGen.SStr(_titg->X2));
290  for (_tith = rSupCandGen.TransRelBegin(currenth); _tith != rSupCandGen.TransRelEnd(currenth); ++_tith)
291  FD_DF("IsControllable: h: " << rSupCandGen.SStr(_tith->X1) << "-"
292  << rSupCandGen.EStr(_tith->Ev) << "-" << rSupCandGen.SStr(_tith->X2));
293 #endif
294 
295  // process all h transitions while there could be matching g transitions
296  TransSet::Iterator titg = rPlantGen.TransRelBegin(currentg);
297  TransSet::Iterator titg_end = rPlantGen.TransRelEnd(currentg);
298  TransSet::Iterator tith = rSupCandGen.TransRelBegin(currenth);
299  TransSet::Iterator tith_end = rSupCandGen.TransRelEnd(currenth);
300  while ((tith != tith_end) && (titg != titg_end)) {
301  FD_DF("IsControllable: processing g-transition: " << rPlantGen.SStr(titg->X1)
302  << "-" << rPlantGen.EStr(titg->Ev) << "-" << rPlantGen.SStr(titg->X2));
303  FD_DF("IsControllable: processing h-transition: " << rSupCandGen.SStr(tith->X1)
304  << "-" << rSupCandGen.EStr(tith->Ev) << "-" << rSupCandGen.SStr(tith->X2));
305  // increment tith and titg case A: process common events
306  if (titg->Ev == tith->Ev) {
307  FD_DF("IsControllable: processing common event " << rPlantGen.EStr(titg->Ev));
308  // form next state and add to stack
309  std::pair<Idx,Idx> next = std::make_pair(titg->X2,tith->X2);
310  // add to todo list if not processed so far
311  if(processed.find(next)==processed.end()) {
312  FD_DF("IsControllable: todo push: (" << rPlantGen.SStr(titg->X2) << "|"
313  << rSupCandGen.SStr(tith->X2) << ")");
314  todo.push(next);
315  }
316  // proceed
317  ++titg;
318  ++tith;
319  }
320  // increment tith and titg case B: process g event that is not enabled in h
321  else if (titg->Ev < tith->Ev) {
322  FD_DF("IsControllable: asynchronous execution of event "
323  << rPlantGen.EStr(titg->Ev) << " in g while " << rSupCandGen.EStr(tith->Ev)
324  << " in h");
325  // if uncontrollable transition violates specification
326  // record that state as critical
327  if (!rCAlph.Exists(titg->Ev)) {
328  FD_DF("IsControllable: asynchronous event " << rPlantGen.EStr(titg->Ev)
329  << " in g is uncontrollable");
330  FD_DF("IsControllable: TraverseUncontrollableBackwards(" << rSupCandGen.SStr(currenth) << ")");
331  rCriticalStates.Insert(currenth);
332  // exit all loops over g transrel
333  titg = titg_end;
334  break;
335  }
336  FD_DF("IsControllable: incrementing g transrel");
337  ++titg;
338  }
339  // increment tith and titg case C: process h event that is not enabled in g
340  else {
341  // #ifdef FAUDES_CHECKED
342  // FD_WARN("IsControllable: transition " << rSupCandGen.TStr(*tith)
343  // << " in specification h not found in g");
344  // #endif
345  FD_DF("IsControllable: incrementing h transrel");
346  ++tith;
347  }
348  } // end while tith and titg
349  // increment tith and titg case D: process leftover g events
350  while (titg != titg_end) {
351  FD_DF("IsControllable: asynchronous execution of event "
352  << rPlantGen.EStr(titg->Ev) << " in g at end of h");
353  FD_DF("IsControllable: actual g-transition: " << rPlantGen.SStr(titg->X1)
354  << "-" << rPlantGen.EStr(titg->Ev) << "-" << rPlantGen.SStr(titg->X2));
355  FD_DF("IsControllable: actual h-transition: end");
356  // if uncontrollable transition violates specification
357  if (!rCAlph.Exists(titg->Ev)) {
358  FD_DF("IsControllable: asynchronous execution of uncontrollable event "
359  << rPlantGen.EStr(titg->Ev) << " in g");
360  FD_DF("IsControllable: TraverseUncontrollableBackwards(" << rPlantGen.SStr(currenth) << ")");
361  rCriticalStates.Insert(currenth);
362  // exit this loop
363  break;
364  }
365  FD_DF("IsControllable: incrementing g transrel");
366  ++titg;
367  }
368  //#ifdef FAUDES_CHECKED
369  // increment tith and titg case E: process leftover h events
370  //while (tith != tith_end) {
371  // FD_WARN("IsControllable: transition " << rSupCandGen.TStr(*tith) << " in specification h not found in g");
372  // FD_DF("IsControllable: incrementing h transrel");
373  // ++tith;
374  //}
375  //#endif
376  } //end while todo
377 
378 
379  // return identified critical states
380  return rCriticalStates.Empty();
381 }
382 
383 
384 
385 // SupConProduct(rPlantGen, rCAlph, rSpecGen, rCompositionMap, rResGen)
386 void SupConProduct(
387  const Generator& rPlantGen,
388  const EventSet& rCAlph,
389  const Generator& rSpecGen,
390  std::map< std::pair<Idx,Idx>, Idx>& rCompositionMap,
391  Generator& rResGen)
392 {
393  FD_DF("SupConProduct(" << &rPlantGen << "," << &rSpecGen << ")");
394 
395  // HELPERS:
396 
397  // todo stack
398  std::stack< std::pair<Idx,Idx> > todo;
399  // set of critical states
400  StateSet critical;
401  // current state, next state, as pair
402  std::pair<Idx,Idx> currentp, nextp;
403  // current state, next state, at result
404  Idx currentt, nextt;
405  std::map< std::pair<Idx,Idx>, Idx>::iterator rcmapit;
406  StateSet::Iterator lit1, lit2;
407  TransSet::Iterator titg, titg_end, tith, tith_end;
408 
409  // prepare
410  rResGen.ClearStates();
411  rCompositionMap.clear();
412 
413  // ALGORITHM:
414  if (rPlantGen.InitStatesEmpty()) {
415  FD_DF("SupConProduct: plant got no initial states. "
416  << "parallel composition contains empty language.");
417  return;
418  }
419  if (rSpecGen.InitStatesEmpty()) {
420  FD_DF("SupConProduct: spec got no initial states. "
421  << "parallel composition contains empty language.");
422  return;
423  }
424 
425  // create initial state
426  currentp = std::make_pair(*rPlantGen.InitStatesBegin(), *rSpecGen.InitStatesBegin());
427  todo.push(currentp);
428  rCompositionMap[currentp] = rResGen.InsInitState();
429  FD_DF("SupConProduct: insert initial state: ("
430  << rPlantGen.SStr(currentp.first)
431  << "|" << rSpecGen.SStr(currentp.second) << ") as idx "
432  << rCompositionMap[currentp]);
433  if(rPlantGen.ExistsMarkedState(*rPlantGen.InitStatesBegin())
434  && rSpecGen.ExistsMarkedState(*rSpecGen.InitStatesBegin())) {
435  rResGen.SetMarkedState(rCompositionMap[currentp]);
436  FD_DF("SupConProduct: initial state is marked");
437  }
438 
439  // do parallel composition of reachable states while avoiding critical states
440  // this creates an accessible generator
441 
442  FD_DF("SupConProduct: *** processing reachable states ***");
443  while (! todo.empty()) {
444  // allow for user interrupt
445  // LoopCallback();
446  // allow for user interrupt, incl progress report
447  FD_WPC(rCompositionMap.size(),rCompositionMap.size()+todo.size(),"SupConProduct(): processing");
448  // get next reachable pair of states from todo stack
449  currentp = todo.top();
450  todo.pop();
451  currentt = rCompositionMap[currentp];
452  FD_DF("SupConProduct: todo pop: ("
453  << rPlantGen.SStr(currentp.first)
454  << "|" << rSpecGen.SStr(currentp.second) << ") as idx "
455  << currentt);
456  // might have been indicated to be critical
457  if(critical.Exists(currentt)) continue;
458  // set up transition relation iterators
459  titg = rPlantGen.TransRelBegin(currentp.first);
460  titg_end = rPlantGen.TransRelEnd(currentp.first);
461  tith = rSpecGen.TransRelBegin(currentp.second);
462  tith_end = rSpecGen.TransRelEnd(currentp.second);
463 
464 #ifdef FAUDES_DEBUG_FUNCTION
465  // print all transitions of current states
466  FD_DF("SupConParallel: transitions from current state:");
467  for (;titg != titg_end; ++titg)
468  FD_DF("SupConParallel: g: " << rPlantGen.TStr(*titg));
469  for (;tith != tith_end; ++tith) {
470  FD_DF("SupConParallel: h: " << rSpecGen.TStr(*tith));
471  }
472  titg = rPlantGen.TransRelBegin(currentp.first);
473  tith = rSpecGen.TransRelBegin(currentp.second);
474 #endif
475 
476  // process all h transitions while there could be matching g transitions
477  while((tith != tith_end) && (titg != titg_end)) {
478  FD_DF("SupConProduct: current g-transition: " << rPlantGen.TStr(*titg) );
479  FD_DF("SupConProduct: current h-transition: " << rSpecGen.TStr(*tith));
480 
481  // case A: execute common events
482  if(titg->Ev == tith->Ev) {
483  FD_DF("SupConProduct: executing common event " << rPlantGen.EStr(titg->Ev));
484  nextp = std::make_pair(titg->X2, tith->X2);
485  rcmapit = rCompositionMap.find(nextp);
486  // if state is new ...
487  if(rcmapit == rCompositionMap.end()) {
488  // ... add on todo stack
489  todo.push(nextp);
490  // ... insert in result
491  nextt = rResGen.InsState();
492  rCompositionMap[nextp] = nextt;
493  FD_DF("SupConProduct: insert state: (" <<
494  rPlantGen.SStr(nextp.first) << "|"
495  << rSpecGen.SStr(nextp.second) << ") as idx "
496  << nextt);
497  // .. mark on the fly
498  if(rPlantGen.ExistsMarkedState(nextp.first) &&
499  rSpecGen.ExistsMarkedState(nextp.second)) {
500  rResGen.SetMarkedState(nextt);
501  FD_DF("SupConProduct: marked nes state")
502  }
503  }
504  // if state already exists
505  else {
506  nextt = rcmapit->second;
507  }
508  // if successor state is not critical add transition and proceed
509  if(!critical.Exists(nextt)) {
510  FD_DF("SupConProduct: set transition " <<
511  rResGen.TStr(Transition(currentt,titg->Ev,nextt)));
512  rResGen.SetTransition(currentt, titg->Ev, nextt);
513  FD_DF("SupConProduct: incrementing g and h transrel");
514  ++titg;
515  ++tith;
516  }
517  // if successor state is critical and event is uncontrollable then this state becomes critical, too
518  else if (!rCAlph.Exists(titg->Ev)) {
519  FD_DF("SupConProduct: successor in critical with uncntr. shared event " << rSpecGen.EStr(titg->Ev))
520  FD_DF("SupConProduct: critical insert, exit loop");
521  critical.Insert(currentt);
522  // exit all loops
523  titg = titg_end;
524  tith = tith_end;
525  }
526  // else if successor state is critical and event controllable we may proceed
527  else {
528  FD_DF("SupConProduct: incrementing g and h transrel");
529  ++titg;
530  ++tith;
531  }
532  } // end: shared event (case A)
533 
534  // case B: process g event that is not enabled for h
535  else if (titg->Ev < tith->Ev) {
536  FD_DF("SupConProduct: event only enabled in g: " << rPlantGen.EStr(titg->Ev));
537  // when uncontrollable, current state is critical
538  if(!rCAlph.Exists(titg->Ev)) {
539  FD_DF("SupConProduct: asynchronous event is uncontrollable, critical insert, exit loop");
540  critical.Insert(currentt);
541  // exit all loops
542  titg = titg_end;
543  tith = tith_end;
544  break;
545  }
546  FD_DF("SupConProduct: incrementing g transrel");
547  ++titg;
548  }
549 
550  // case C: process h event that is not enabled for g
551  else {
552  FD_DF("SupConProduct: incrementing h transrel");
553  ++tith;
554  }
555  } // end while incrementing both tith and titg
556 
557  // case D: process leftover events of g
558  while (titg != titg_end) {
559  FD_DF("SupConProduct: event only enabled in g: " << rPlantGen.EStr(titg->Ev));
560  // if uncontrollable transition leaves specification
561  if (!rCAlph.Exists(titg->Ev)) {
562  FD_DF("SupConProduct: asynchronous event is uncontrollable, critical insert, exit loop");
563  critical.Insert(currentt);
564  // exit all loops
565  break;
566  }
567  FD_DF("SupConProduct: incrementing g transrel");
568  ++titg;
569  }
570  //#ifdef FAUDES_CHECKED
571  // increment titg and titg, case E: process leftover events of h
572  //while (txoith != tith_end) {
573  // FD_WARN("SupConProduct: transition " << rSpecGen.TStr(*tith) << " in specification h not found in g");
574  // FD_DF("SupConProduct: incrementing h transrel");
575  // ++tith;
576  //}
577  //#endif
578  } // while todo
579  FD_DF("SupConProduct: deleting critical states...");
580  rResGen.DelStates(critical);
581 }
582 
583 
584 
585 // SupConNBUnchecked(rPlantGen, rCAlph, rSpecGen, rCompositionMap, rResGen)
586 void SupConNBUnchecked(
587  const Generator& rPlantGen,
588  const EventSet& rCAlph,
589  const Generator& rSpecGen,
590  std::map< std::pair<Idx,Idx>, Idx>& rCompositionMap,
591  Generator& rResGen)
592 {
593  FD_DF("SupConNB(" << &rPlantGen << "," << &rSpecGen << ")");
594 
595  // PREPARE RESULT:
596  Generator* pResGen = &rResGen;
597  if(&rResGen== &rPlantGen || &rResGen== &rSpecGen) {
598  pResGen= rResGen.New();
599  }
600  pResGen->Clear();
601  pResGen->Name(CollapsString("SupConNB(("+rPlantGen.Name()+"),("+rSpecGen.Name()+"))"));
602  pResGen->InjectAlphabet(rPlantGen.Alphabet());
603 
604  // controllable events
605  FD_DF("SupConNB: controllable events: " << rCAlph.ToString());
606 
607  // ALGORITHM:
608  SupConProduct(rPlantGen, rCAlph, rSpecGen, rCompositionMap, *pResGen);
609 
610  // make resulting generator trim until it's fully controllable
611  while(true) {
612  if(pResGen->Empty()) break;
613  Idx state_num = pResGen->Size();
614  SupConClosedUnchecked(rPlantGen, rCAlph, *pResGen);
615  pResGen->Trim();
616  if(pResGen->Size() == state_num) break;
617  }
618 
619  // convenience state names
620  if(rPlantGen.StateNamesEnabled() && rSpecGen.StateNamesEnabled() && rResGen.StateNamesEnabled())
621  SetComposedStateNames(rPlantGen, rSpecGen, rCompositionMap, *pResGen);
622  else
623  pResGen->StateNamesEnabled(false);
624 
625  // copy result
626  if(pResGen != &rResGen) {
627  pResGen->Move(rResGen);
628  delete pResGen;
629  }
630 
631 }
632 
633 // ControlProblemConsistencyCheck(rPlantGen, rCAlph, rSpecGen)
634 void ControlProblemConsistencyCheck(
635  const Generator& rPlantGen,
636  const EventSet& rCAlph,
637  const Generator& rSpecGen)
638 {
639 
640  // alphabets must match
641  if ( rPlantGen.Alphabet() != rSpecGen.Alphabet()) {
642  EventSet only_in_plant = rPlantGen.Alphabet() - rSpecGen.Alphabet();
643  EventSet only_in_spec = rSpecGen.Alphabet() - rPlantGen.Alphabet();
644  only_in_plant.Name("Only_In_Plant");
645  only_in_spec.Name("Only_In_Specification");
646  std::stringstream errstr;
647  errstr << "Alphabets of generators do not match.";
648  if(!only_in_plant.Empty())
649  errstr << " " << only_in_plant.ToString() << ".";
650  if(!only_in_spec.Empty())
651  errstr << " " << only_in_spec.ToString() << ".";
652  throw Exception("SupCon/SupConNB", errstr.str(), 100);
653  }
654 
655  // controllable events have to be subset of Sigma
656  if(!(rCAlph<=rPlantGen.Alphabet())) {
657  EventSet only_in_CAlph = rCAlph - rPlantGen.Alphabet();
658  std::stringstream errstr;
659  errstr << "Not all controllable events are contained in Sigma: "
660  << only_in_CAlph.ToString() << ".";
661  throw Exception("ControllProblemConsistencyCheck", errstr.str(), 100);
662  }
663 
664  // TODO: check symboltables to match
665 
666  // plant and spec must be deterministic
667  bool plant_det = rPlantGen.IsDeterministic();
668  bool spec_det = rSpecGen.IsDeterministic();
669 
670  if ((plant_det == false) && (spec_det == true)) {
671  std::stringstream errstr;
672  errstr << "Plant generator must be deterministic, "
673  << "but is nondeterministic";
674  throw Exception("ControllableConsistencyCheck", errstr.str(), 201);
675  }
676  else if ((plant_det == true) && (spec_det == false)) {
677  std::stringstream errstr;
678  errstr << "Spec generator must be deterministic, "
679  << "but is nondeterministic";
680  throw Exception("ControllableConsistencyCheck", errstr.str(), 203);
681  }
682  else if ((plant_det == false) && (spec_det == false)) {
683  std::stringstream errstr;
684  errstr << "Plant and spec generator must be deterministic, "
685  << "but both are nondeterministic";
686  throw Exception("ControllableConsistencyCheck", errstr.str(), 204);
687  }
688 }
689 
690 // ControlProblemConsistencyCheck(rPlantGen, rCAlph, rSpecGen)
691 void ControlProblemConsistencyCheck(
692  const Generator& rPlantGen,
693  const EventSet& rCAlph,
694  const EventSet& rOAlph,
695  const Generator& rSpecGen)
696 {
697  // std test
698  ControlProblemConsistencyCheck(rPlantGen,rCAlph,rSpecGen);
699  // observable events have to be subset of Sigma
700  if(!(rOAlph<=rPlantGen.Alphabet())) {
701  EventSet only_in_OAlph = rOAlph - rPlantGen.Alphabet();
702  std::stringstream errstr;
703  errstr << "Not all observable events are contained in Sigma: "
704  << only_in_OAlph.ToString() << ".";
705  throw Exception("ControllProblemConsistencyCheck", errstr.str(), 100);
706  }
707 }
708 
709 
710 /*
711 ****************************************
712 * SUPCON: WRAPPER / USER FUNCTIONS *
713 ****************************************
714 */
715 
716 
717 // IsControllable(rPlantGen, rCAlph, rSupCandGen)
718 bool IsControllable(
719  const Generator& rPlantGen,
720  const EventSet& rCAlph,
721  const Generator& rSupCandGen)
722 {
723  FD_DF("IsControllable(" << &rSupCandGen << "," << &rPlantGen << ")");
724 
725  // HELPERS:
726  FD_DF("IsControllable: controllable events: " << rCAlph.ToString());
727 
728  // critical set
729  StateSet critical;
730 
731  // CONSISTENCY CHECKS:
732  ControlProblemConsistencyCheck(rPlantGen, rCAlph, rSupCandGen);
733 
734  // ALGORITHM:
735  return IsControllableUnchecked(rPlantGen, rCAlph, rSupCandGen, critical);
736 }
737 
738 
739 // IsControllable(rPlantGen, rCAlph, rSupCandGen, critical)
740 bool IsControllable(
741  const Generator& rPlantGen,
742  const EventSet& rCAlph,
743  const Generator& rSupCandGen,
744  StateSet& rCriticalStates)
745 {
746  FD_DF("IsControllable(" << &rSupCandGen << "," << &rPlantGen << ")");
747 
748  // CONSISTENCY CHECKS:
749  ControlProblemConsistencyCheck(rPlantGen, rCAlph, rSupCandGen);
750 
751  // ALGORITHM:
752  return IsControllableUnchecked(rPlantGen, rCAlph, rSupCandGen, rCriticalStates);
753 }
754 
755 
756 // SupConNB(rPlantGen, rCAlph, rSpecGen, rResGen)
757 void SupConNB(
758  const Generator& rPlantGen,
759  const EventSet& rCAlph,
760  const Generator& rSpecGen,
761  Generator& rResGen)
762 {
763 
764  // CONSISTENCY CHECK:
765  ControlProblemConsistencyCheck(rPlantGen, rCAlph, rSpecGen);
766 
767  // HELPERS:
768  std::map< std::pair<Idx,Idx>, Idx> rcmap;
769 
770  // ALGORITHM:
771  SupConNBUnchecked(rPlantGen, rCAlph, rSpecGen, rcmap, rResGen);
772 }
773 
774 
775 
776 
777 // SupConClosed(rPlantGen, rCAlph, rSpecGen, rResGen)
778 void SupConClosed(
779  const Generator& rPlantGen,
780  const EventSet& rCAlph,
781  const Generator& rSpecGen,
782  Generator& rResGen)
783 {
784  // HELPERS:
785  std::map< std::pair<Idx,Idx>, Idx> rcmap;
786 
787  // ALGORITHM:
788  SupConClosed(rPlantGen, rCAlph, rSpecGen, rcmap, rResGen);
789 }
790 
791 
792 // SupConClosed(rPlantGen, rCAlph, rSpecGen, rCompositionMap, rResGen)
793 void SupConClosed(
794  const Generator& rPlantGen,
795  const EventSet& rCAlph,
796  const Generator& rSpecGen,
797  std::map< std::pair<Idx,Idx>, Idx>& rCompositionMap,
798  Generator& rResGen)
799 {
800  FD_DF("SupConClosed(" << &rPlantGen << "," << &rSpecGen << ")");
801 
802  // PREPARE RESULT:
803 
804  // prepare result
805  Generator* pResGen = &rResGen;
806  if(&rResGen== &rPlantGen || &rResGen== &rSpecGen) {
807  pResGen= rResGen.New();
808  }
809  pResGen->Clear();
810  pResGen->Name(CollapsString("SupConClosed(("+rPlantGen.Name()+"),("+rSpecGen.Name()+"))"));
811  pResGen->InjectAlphabet(rPlantGen.Alphabet());
812 
813  // HELPERS:
814  FD_DF("SupCon: controllable events: " << rCAlph.ToString());
815 
816  // CONSISTENCY CHECK:
817  ControlProblemConsistencyCheck(rPlantGen, rCAlph, rSpecGen);
818 
819  // ALGORITHM:
820 
821  // product composition
822  SupConProduct(rPlantGen, rCAlph, rSpecGen, rCompositionMap, *pResGen);
823  // make resulting generator controllable
824  SupConClosedUnchecked(rPlantGen, rCAlph, *pResGen);
825 
826  // restrict composition map
827  std::map< std::pair<Idx,Idx>, Idx>::iterator rcmapit = rCompositionMap.begin();
828  while(rcmapit != rCompositionMap.end())
829  if(!rResGen.ExistsState(rcmapit->second)) rCompositionMap.erase(rcmapit++);
830  else rcmapit++;
831 
832  // convenience state names
833  if (rPlantGen.StateNamesEnabled() && rSpecGen.StateNamesEnabled() && rResGen.StateNamesEnabled())
834  SetComposedStateNames(rPlantGen, rSpecGen, rCompositionMap, *pResGen);
835  else
836  pResGen->StateNamesEnabled(false);
837 
838  // copy result
839  if(pResGen != &rResGen) {
840  pResGen->Move(rResGen);
841  delete pResGen;
842  }
843 }
844 
845 
846 // TraverseUncontrollableBackwards(rCAlph, rtransrel, critical, current)
847 void TraverseUncontrollableBackwards(
848  const EventSet& rCAlph,
849  TransSetX2EvX1& rtransrel,
850  StateSet& rCriticalStates,
851  Idx current) {
852  FD_DF("TraverseUncontrollableBackwards: " << rCriticalStates.Str(current));
853 
854  // HELPERS:
855  std::stack<Idx> todo;
856  TransSetX2EvX1::Iterator rtit = rtransrel.BeginByX2(current);
857  TransSetX2EvX1::Iterator rtit_end = rtransrel.EndByX2(current);
858 
859  // ALGORITHM:
860  rCriticalStates.Insert(current);
861  todo.push(current);
862  FD_DF("TraverseUncontrollableBackwards: current rCriticalStates set: "
863  << rCriticalStates.ToString());
864  // process todo stack
865  while(! todo.empty()) {
866  // get top state from todo stack
867  current = todo.top(); todo.pop();
868  // iteration over all transitions with x2 == current
869  rtit_end = rtransrel.EndByX2(current);
870  rtit = rtransrel.BeginByX2(current);
871  for(; rtit != rtit_end; ++rtit) {
872  // if uncontrollable event and predecessor state not already critical
873  if((!rCAlph.Exists(rtit->Ev)) && (! rCriticalStates.Exists(rtit->X1))) {
874  FD_DF("TraverseUncontrollableBackwards: todo push " << rCriticalStates.Str(rtit->X1));
875  todo.push(rtit->X1);
876  FD_DF("TraverseUncontrollableBackwards: critical insert: " << rCriticalStates.Str(rtit->X1));
877  rCriticalStates.Insert(rtit->X1);
878  }
879  }
880  } // end while todo
881 }
882 
883 
884 // controllability test for System plant
885 bool IsControllable(
886  const System& rPlantGen,
887  const Generator& rSupCandGen)
888 {
889  return IsControllable(rPlantGen, rPlantGen.ControllableEvents(), rSupCandGen);
890 }
891 
892 
893 // supcon for Systems:
894 // uses and maintains controllablity from plant
895 void SupConNB(
896  const System& rPlantGen,
897  const Generator& rSpecGen,
898  Generator& rResGen) {
899 
900  // prepare result
901  Generator* pResGen = &rResGen;
902  if(&rResGen== &rPlantGen || &rResGen== &rSpecGen) {
903  pResGen= rResGen.New();
904  }
905 
906  // execute
907  SupConNB(rPlantGen, rPlantGen.ControllableEvents(),rSpecGen,*pResGen);
908 
909  // copy all attributes of input alphabet
910  pResGen->EventAttributes(rPlantGen.Alphabet());
911 
912  // copy result
913  if(pResGen != &rResGen) {
914  pResGen->Move(rResGen);
915  delete pResGen;
916  }
917 
918 }
919 
920 // supcon for Systems
921 // uses and maintains controllablity from plant
922 void SupConClosed(
923  const System& rPlantGen,
924  const Generator& rSpecGen,
925  Generator& rResGen) {
926 
927  // prepare result
928  Generator* pResGen = &rResGen;
929  if(&rResGen== &rPlantGen || &rResGen== &rSpecGen) {
930  pResGen= rResGen.New();
931  }
932 
933  // execute
934  SupConClosed(rPlantGen, rPlantGen.ControllableEvents(),rSpecGen,*pResGen);
935 
936  // copy all attributes of input alphabet
937  pResGen->EventAttributes(rPlantGen.Alphabet());
938 
939  // copy result
940  if(pResGen != &rResGen) {
941  pResGen->Move(rResGen);
942  delete pResGen;
943  }
944 
945 }
946 
947 } // name space
FD_WPC
#define FD_WPC(cntnow, contdone, message)
Application callback: optional write progress report to console or application, incl count
Definition: cfl_definitions.h:107
FD_DF
#define FD_DF(message)
Debug: optional report on user functions.
Definition: cfl_definitions.h:138
faudes::Exception
Faudes exception class.
Definition: cfl_exception.h:118
faudes::IndexSet
Set of indices.
Definition: cfl_indexset.h:78
faudes::IndexSet::Str
std::string Str(const Idx &rIndex) const
Return pretty printable index.
Definition: cfl_indexset.h:185
faudes::IndexSet::Insert
Idx Insert(void)
Insert new index to set.
Definition: cfl_indexset.cpp:313
faudes::NameSet
Set of indices with symbolic names.
Definition: cfl_nameset.h:69
faudes::NameSet::Exists
bool Exists(const Idx &rIndex) const
Test existence of index.
Definition: cfl_nameset.cpp:433
faudes::TBaseSet::Iterator
Iterator class for high-level api to TBaseSet.
Definition: cfl_baseset.h:387
faudes::TTransSet
Set of Transitions.
Definition: cfl_transset.h:242
faudes::TTransSet::BeginByX2
Iterator BeginByX2(Idx x2) const
Iterator to first Transition specified by successor state x2.
Definition: cfl_transset.h:1385
faudes::TTransSet::Insert
bool Insert(const Transition &rTransition)
Add a Transition.
Definition: cfl_transset.h:1470
faudes::TTransSet::EndByX2
Iterator EndByX2(Idx x2) const
Iterator to first Transition after specified successor state x2.
Definition: cfl_transset.h:1396
faudes::TTransSet< TransSort::X1EvX2 >::Iterator
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Iterator on transition.
Definition: cfl_transset.h:269
faudes::TaGenerator::Alphabet
const TaEventSet< EventAttr > & Alphabet(void) const
Return const reference to alphabet.
Definition: cfl_agenerator.h:1358
faudes::TcGenerator
Generator with controllability attributes.
Definition: cfl_cgenerator.h:273
faudes::TcGenerator::ControllableEvents
EventSet ControllableEvents(void) const
Get EventSet with controllable events.
Definition: cfl_cgenerator.h:1124
faudes::Transition
Triple (X1,Ev,X2) to represent current state, event and next state.
Definition: cfl_transset.h:57
faudes::Type::ToString
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
Write configuration data to a string.
Definition: cfl_types.cpp:169
faudes::vGenerator
Base class of all FAUDES generators.
Definition: cfl_generator.h:213
faudes::vGenerator::InitStatesBegin
StateSet::Iterator InitStatesBegin(void) const
Iterator to Begin() of mInitStates.
Definition: cfl_generator.cpp:1150
faudes::vGenerator::SetTransition
bool SetTransition(Idx x1, Idx ev, Idx x2)
Add a transition to generator by indices.
Definition: cfl_generator.cpp:1626
faudes::vGenerator::Alphabet
const EventSet & Alphabet(void) const
Return const reference to alphabet.
Definition: cfl_generator.cpp:1878
faudes::vGenerator::Move
virtual void Move(vGenerator &rGen)
Destructive copy to other vGenerator.
Definition: cfl_generator.cpp:333
faudes::vGenerator::InitStatesEmpty
bool InitStatesEmpty(void) const
Check if set of initial states are empty.
Definition: cfl_generator.cpp:663
faudes::vGenerator::TransRelBegin
TransSet::Iterator TransRelBegin(void) const
Iterator to Begin() of transition relation.
Definition: cfl_generator.cpp:1067
faudes::vGenerator::Trim
bool Trim(void)
Make generator trim.
Definition: cfl_generator.cpp:2122
faudes::vGenerator::ClearStates
void ClearStates(void)
Clear all states and transitions, maintain alphabet.
Definition: cfl_generator.cpp:624
faudes::vGenerator::New
virtual vGenerator * New(void) const
Construct on heap.
Definition: cfl_generator.cpp:168
faudes::vGenerator::ExistsState
bool ExistsState(Idx index) const
Test existence of state in state set.
Definition: cfl_generator.cpp:1776
faudes::vGenerator::TStr
std::string TStr(const Transition &rTrans) const
Return pretty printable transition (eg for debugging)
Definition: cfl_generator.cpp:3841
faudes::vGenerator::Name
void Name(const std::string &rName)
Set the generator's name.
Definition: cfl_generator.cpp:526
faudes::vGenerator::DelStates
void DelStates(const StateSet &rDelStates)
Delete a set of states Cleans mpStates, mInitStates, mMarkedStates, mpTransrel, and mpStateSymboltabl...
Definition: cfl_generator.cpp:1381
faudes::vGenerator::TransRelEnd
TransSet::Iterator TransRelEnd(void) const
Iterator to End() of transition relation.
Definition: cfl_generator.cpp:1072
faudes::vGenerator::IsDeterministic
bool IsDeterministic(void) const
Check if generator is deterministic.
Definition: cfl_generator.cpp:2367
faudes::vGenerator::EStr
std::string EStr(Idx index) const
Pretty printable event name for index (eg for debugging).
Definition: cfl_generator.cpp:3828
faudes::vGenerator::InsState
Idx InsState(void)
Add new anonymous state to generator.
Definition: cfl_generator.cpp:1247
faudes::vGenerator::SetMarkedState
void SetMarkedState(Idx index)
Set an existing state as marked state by index.
Definition: cfl_generator.cpp:1507
faudes::vGenerator::Empty
bool Empty(void) const
Check if generator is empty (no states)
Definition: cfl_generator.cpp:653
faudes::vGenerator::InsInitState
Idx InsInitState(void)
Create new anonymous state and set as initial state.
Definition: cfl_generator.cpp:1287
faudes::vGenerator::EventAttributes
virtual void EventAttributes(const EventSet &rEventSet)
Set attributes for existing events.
Definition: cfl_generator.cpp:1730
faudes::vGenerator::StateNamesEnabled
bool StateNamesEnabled(void) const
Whether libFAUEDS functions are requested to generate state names.
Definition: cfl_generator.cpp:999
faudes::vGenerator::Size
Idx Size(void) const
Get generator size (number of states)
Definition: cfl_generator.cpp:577
faudes::vGenerator::SStr
std::string SStr(Idx index) const
Return pretty printable state name for index (eg for debugging)
Definition: cfl_generator.cpp:3834
faudes::vGenerator::Clear
virtual void Clear(void)
Clear generator data.
Definition: cfl_generator.cpp:582
faudes::vGenerator::ExistsMarkedState
bool ExistsMarkedState(Idx index) const
Test existence of state in mMarkedStates.
Definition: cfl_generator.cpp:1806
faudes::vGenerator::States
const StateSet & States(void) const
Return reference to state set.
Definition: cfl_generator.cpp:1883
faudes::vGenerator::InjectAlphabet
void InjectAlphabet(const EventSet &rNewalphabet)
Set mpAlphabet without consistency check.
Definition: cfl_generator.cpp:1170
faudes::TBaseSet::Empty
bool Empty(void) const
Test whether if the TBaseSet is Empty.
Definition: cfl_baseset.h:1824
faudes::TBaseSet::Exists
bool Exists(const T &rElem) const
Test existence of element.
Definition: cfl_baseset.h:2115
faudes::TBaseSet::Clear
virtual void Clear(void)
Clear all set.
Definition: cfl_baseset.h:1902
faudes::TBaseSet::Name
const std::string & Name(void) const
Return name of TBaseSet.
Definition: cfl_baseset.h:1755
faudes::IsControllable
bool IsControllable(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSupCandGen)
Test controllability.
Definition: syn_supcon.cpp:718
faudes::SupConNB
void SupConNB(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
Nonblocking Supremal Controllable Sublanguage.
Definition: syn_supcon.cpp:757
faudes::SupConClosed
void SupConClosed(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
Supremal Controllable and Closed Sublanguage.
Definition: syn_supcon.cpp:778
faudes
libFAUDES resides within the namespace faudes.
Definition: cfl_agenerator.h:43
faudes::Idx
uint32_t Idx
Type definition for index type (allways 32bit)
Definition: cfl_definitions.h:43
faudes::SetComposedStateNames
void SetComposedStateNames(const Generator &rGen1, const Generator &rGen2, const std::map< std::pair< Idx, Idx >, Idx > &rCompositionMap, Generator &rGen12)
Helper: uses composition map to track state names in a paralell composition.
Definition: cfl_parallel.cpp:654
faudes::SupConProduct
void SupConProduct(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, std::map< std::pair< Idx, Idx >, Idx > &rCompositionMap, Generator &rResGen)
Parallel composition optimized for the purpose of SupCon (internal function)
Definition: syn_supcon.cpp:386
faudes::CollapsString
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
faudes::ControlProblemConsistencyCheck
void ControlProblemConsistencyCheck(const GeneratorVector &rPlantGenVec, const EventSet &rConAlph, const GeneratorVector &rSpecGenVec)
Compositional synthesis.
Definition: syn_compsyn.cpp:1301
faudes::SupConClosedUnchecked
void SupConClosedUnchecked(const Generator &rPlantGen, const EventSet &rCAlph, Generator &rSupCandGen)
Supremal Controllable Sublangauge (internal function)
Definition: syn_supcon.cpp:57
faudes::SupConNBUnchecked
void SupConNBUnchecked(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, std::map< std::pair< Idx, Idx >, Idx > &rCompositionMap, Generator &rResGen)
Nonblocking Supremal Controllable Sublanguage (internal function)
Definition: syn_supcon.cpp:586
faudes::TraverseUncontrollableBackwards
void TraverseUncontrollableBackwards(const EventSet &rCAlph, TransSetX2EvX1 &rtransrel, StateSet &rCriticalStates, Idx current)
Helper function for IsControllable.
Definition: syn_supcon.cpp:847
faudes::IsControllableUnchecked
bool IsControllableUnchecked(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSupCandGen, StateSet &rCriticalStates)
Controllability (internal function)
Definition: syn_supcon.cpp:243
syn_supcon.h
Supremal controllable sublanguage.

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

>>