hio_functions.h
Go to the documentation of this file.
1 /** @file hio_functions.h Algorithms for hierarchical discrete event systems with inputs and outputs */
2 
3 /* Hierarchical IO Systems Plug-In for FAU Discrete Event Systems Library (libfaudes)
4 
5  Copyright (C) 2006 Sebastian Perk
6  Copyright (C) 2006 Thomas Moor
7  Copyright (C) 2006 Klaus Schmidt
8 
9 */
10 
11 
12 #ifndef FAUDES_HIO_FUNCTIONS_H
13 #define FAUDES_HIO_FUNCTIONS_H
14 
15 #include "hio_constraint.h"
16 #include "hio_plant.h"
17 #include "hio_controller.h"
18 #include "hio_environment.h"
19 #include "corefaudes.h"
20 #include <vector>
21 #include <stack>
22 #include <map>
23 
24 namespace faudes {
25 
26 /**
27  * CompleteSynth: compute supremal complete and
28  * controllable (and closed) sublanguage.
29  * Computes the supremal complete and
30  * controllable (and closed) sublanguage of the
31  * language generated by rSpec wrt the language
32  * generated by rPlant and the controllable events
33  * rCalph.
34  * Method: iteration of SupCon() and erasing of dead
35  * states found by IsComplete until a fix point is
36  * reached.
37  * Leads to maximal solution as shown in:
38  * Kumar, Garg, Marcus. "On Supervisory Control of
39  * sequential behaviors" IEEE Transactions On
40  * Automatic Control, Vol. 37, 1992, pp. 1978-1985
41  *
42  * More concise version SupConComplete() is under
43  * construction, see below.
44  *
45  * @param rPlant
46  * plant generator
47  * @param rCAlph
48  * controllable events
49  * @param rSpec
50  * specification generator
51  * @param rClosedLoop
52  * reference to result
53  *
54  * @return
55  * success (true) for nonempty result
56  *
57  * @exception Exception
58  * - see exceptions of SupCon()
59  *
60  * @ingroup hiosysplugin
61  */
62 
63 extern FAUDES_API bool CompleteSynth(
64  const Generator& rPlant,
65  const EventSet rCAlph,
66  const Generator& rSpec,
67  Generator& rClosedLoop);
68 
69 /**
70  * NormalCompleteSynth: compute normal, complete
71  * and controllable (and closed) sublanguage.
72  * Computes the supremal normal, complete and
73  * controllable (and closed) sublanguage of the
74  * language generated by rSpec wrt the language
75  * generated by rPlant, the controllable events
76  * rCalph and the observable events rOAlph.
77  * Method: iteration of CompleteSynth() and SupNorm()
78  * until a fix point is reached.
79  * Note: Supremality (if existent at all) has not yet been
80  * considered. The proof of existence and construction
81  * of both
82  * -the supremal normal and complete sublanguage and
83  * -the supremal normal and controllable sublanguage
84  * can be found in literature, which gives reason for
85  * hope.
86  *
87  * @param rPlant
88  * plant generator
89  * @param rCAlph
90  * controllable events
91  * @param rOAlph
92  * observable events
93  * @param rSpec
94  * specification generator
95  * @param rClosedLoop
96  * reference to result
97  *
98  * @return
99  * success (true) for nonempty closed loop language
100  *
101  * @exception Exception
102  * - see exceptions of SupCon() and SupNorm()
103  *
104  * @ingroup hiosysplugin
105  *
106  */
107 
108 extern FAUDES_API bool NormalCompleteSynth(
109  Generator& rPlant,
110  const EventSet& rCAlph,
111  const EventSet& rOAlph,
112  const Generator& rSpec,
113  Generator& rClosedLoop);
114 
115 /**
116  * NormalCompleteSynthNB: compute normal, complete,
117  * controllable and nonblocking sublanguage.
118  * Computes a normal, complete, controllable and
119  * nonblocking (and closed) sublanguage of
120  * of the language marked by rSpec wrt the language
121  * marked by rPlant, the controllable events
122  * rCalph and the observable events rOAlph.
123  * Method: iteration of CompleteSynth(), SupNorm()
124  * and Trim() until a fix point is reached.
125  * Note: Supremality (if existent at all) has not yet been
126  * considered.
127  *
128  * @param rPlant
129  * plant generator
130  * @param rCAlph
131  * controllable events
132  * @param rOAlph
133  * observable events
134  * @param rSpec
135  * specification generator
136  * @param rClosedLoop
137  * reference to result
138  *
139  * @return
140  * success (true) for nonempty closed loop language
141  *
142  * @exception Exception
143  * - see exceptions of SupCon() and SupNorm()
144  *
145  * @ingroup hiosysplugin
146  *
147  */
149  Generator& rPlant,
150  const EventSet& rCAlph,
151  const EventSet& rOAlph,
152  const Generator& rSpec,
153  Generator& rClosedLoop);
154 
155 /**
156  * IoSortCL: returns IO-sorting structure required
157  * for closed loops. This structure is the prefix closure of
158  * the language structure [(Yp(Up+YcUcUp))*(YeUe)*]*
159  *
160  * @param rYc
161  * alphabet Yc
162  * @param rUc
163  * alphabet Uc
164  * @param rYp
165  * alphabet Yp
166  * @param rUp
167  * alphabet Up
168  * @param rYe
169  * alphabet Ye
170  * @param rUe
171  * alphabet Ue
172  *
173  * @return
174  * IO-sorting language generator
175  *
176  * @exception Exception
177  * - empty parameter(s) (id 0)
178  * - non-disjoint parameters (id 0)
179  *
180  * @ingroup hiosysplugin
181  *
182  */
183 
185  const EventSet& rYc,
186  const EventSet& rUc,
187  const EventSet& rYp,
188  const EventSet& rUp,
189  const EventSet& rYe,
190  const EventSet& rUe);
191 
192 /**
193  * HioFreeInput: extend generator by obviously missing
194  * input transitions. States of the generator in which a
195  * strict but nonempty subset of the alphabet Input is active
196  * are extended by transitions to an error state (ErrState1,
197  * flag Err) such that now the whole Input alphabet is active in
198  * that state. If the alphabet Output is nonempty, an error
199  * behaviour (Output Input)* is concatenated to the error state
200  * using a second error state (ErrState2, flag Err).
201  * Note that this method only helps making the input free in an
202  * hio system but does not guarantee a free input.
203  * Method: the transition relation of all states with at least
204  * one active AND at least one inactive Input-event is
205  * extended by transitions such that formerly inactive Input-
206  * events lead to the first error state in the result. If the
207  * parameter Output is nonempty, transitions with all
208  * Output-events from first error state to the second error
209  * state, and transitions with all Input-events back to the
210  * first error state are inserted.
211  * Note: states with NO active Input-event are ignored.
212  *
213  * @param rGen
214  * generator
215  * @param rInput
216  * alphabet Input
217  * @param rOutput
218  * alphabet Output
219  * @param rResGen
220  * reference to extended generator (result)
221  * @param rErrState1
222  * symbolic name of first error state; ignored if not
223  * rGen.StateNamesEnabled()
224  * @param rErrState2
225  * symbolic name of second error state; ignored if not
226  * rGen.StateNamesEnabled()
227  * @param rErrState1Idx
228  * index of first error state (result)
229  * @param rErrState2Idx
230  * index of second error state if inserted (result)
231  *
232  * @exception Exception
233  * - empty Input-alphabet or non-disjoint Input and Output (id 0)
234  *
235  * @ingroup hiosysplugin
236  *
237  */
238 
239 extern FAUDES_API void HioFreeInput(
240  const Generator& rGen,
241  const EventSet& rInput,
242  const EventSet& rOutput,
243  Generator& rResGen,
244  const std::string& rErrState1,
245  const std::string& rErrState2,
246  Idx& rErrState1Idx,
247  Idx& rErrState2Idx);
248 
249 /**
250  * HioFreeInput: extend generator by obviously missing
251  * input transitions. States of the generator in which a
252  * strict but nonempty subset of the alphabet Input is active
253  * are extended by transitions to an error state (ErrState1,
254  * flag Err) such that now the whole Input alphabet is active in
255  * that state. If the alphabet Output is nonempty, an error
256  * behaviour (Output Input)* is concatenated to the error state
257  * using a second error state (ErrState2, flag Err).
258  * Note that this method only helps making the input free in an
259  * hio system but does not guarantee a free input.
260  * Method: the transition relation of all states with at least
261  * one active AND at least one inactive Input-event is
262  * extended by transitions such that formerly inactive Input-
263  * events lead to the first error state in the result. If the
264  * parameter Output is nonempty, transitions with all
265  * Output-events from first error state to the second error
266  * state, and transitions with all Input-events back to the
267  * first error state are inserted.
268  * Note: states with NO active Input-event are ignored.
269  *
270  * @param rGen
271  * generator
272  * @param rInput
273  * alphabet Input
274  * @param rOutput
275  * alphabet Output
276  * @param rResGen
277  * reference to extended generator (result)
278  * @param rErrState1
279  * symbolic name of first error state; ignored if not
280  * rGen.StateNamesEnabled()
281  * @param rErrState2
282  * symbolic name of second error state; ignored if not
283  * rGen.StateNamesEnabled()
284  *
285  * @exception Exception
286  * - empty Input-alphabet or non-disjoint Input and Output (id 0)
287  *
288  * @ingroup hiosysplugin
289  *
290  */
291 
292 extern FAUDES_API void HioFreeInput(
293  const Generator& rGen,
294  const EventSet& rInput,
295  const EventSet& rOutput,
296  Generator& rResGen,
297  const std::string& rErrState1,
298  const std::string& rErrState2);
299 
300 /**
301  * HioFreeInput: extend generator by obviously missing
302  * input transitions. States of the generator in which a
303  * strict but nonempty subset of the alphabet Input is active
304  * are extended by transitions to an error state (flag Err)
305  * such that now the whole Input alphabet is active in
306  * that state. If the alphabet Output is nonempty, an error
307  * behaviour (Output Input)* is concatenated to the error state
308  * using a second error state (flag Err).
309  * Note that this method only helps making the input free in an
310  * hio system but does not guarantee a free input.
311  * Method: the transition relation of all states with at least
312  * one active AND at least one inactive Input-event is
313  * extended by transitions such that formerly inactive Input-
314  * events lead to the first error state in the result. If the
315  * parameter Output is nonempty, transitions with all
316  * Output-events from first error state to the second error
317  * state, and transitions with all Input-events back to the
318  * first error state are inserted.
319  * Note: states with NO active Input-event are ignored.
320  *
321  * @param rGen
322  * generator
323  * @param rInput
324  * alphabet Input
325  * @param rOutput
326  * alphabet Output
327  * @param rResGen
328  * reference to extended generator (result)
329  *
330  * @exception Exception
331  * - empty Input-alphabet or non-disjoint Input and Output (id 0)
332  *
333  * @ingroup hiosysplugin
334  *
335  */
336 extern FAUDES_API void HioFreeInput(
337  const Generator& rGen,
338  const EventSet& rInput,
339  const EventSet& rOutput,
340  Generator& rResGen);
341 
342 /**
343  * HioFreeInput: extend HioPlant by obviously missing
344  * input transitions. States of the HioPlant in which a
345  * strict but nonempty subset of the Up- or Ue-alphabet is active
346  * are extended by transitions to an error state such that
347  * now the whole Up- or Ue-alphabet is active in that state.
348  * Note that this method only helps making the input free in an
349  * hio system but does not guarantee a free input.
350  * Method: the transition relation of all states with at least
351  * one active AND at least one inactive Up- or Ue-event is
352  * extended by transitions such that formerly inactive Up- or Ue-
353  * events lead to the Up- or Ue-error state in the result.
354  * Note: states with NO active Up- or Ue-event are ignored.
355  *
356  * @param rPlant
357  * HioPlant
358  * @param rResPlant
359  * reference to extended HioPlant (result)
360  *
361  * @ingroup hiosysplugin
362  *
363  */
364 extern FAUDES_API void HioFreeInput(
365  const HioPlant& rPlant,
366  HioPlant& rResPlant);
367 
368 /**
369  * HioFreeInput: extend HioController by obviously missing
370  * input transitions. States of the HioController in which a
371  * strict but nonempty subset of the Uc- or Yp-alphabet is active
372  * are extended by transitions to an error state such that
373  * now the whole Uc- or Yp-alphabet is active in that state. To
374  * avoid an additional deadlock violating completeness, an error
375  * behaviour (Up Yp)* is concatenated to the error state
376  * using a second error state.
377  * Note that this method only helps making the input free in an
378  * hio system but does not guarantee a free input.
379  * Method: the transition relation of all states with at least
380  * one active AND at least one inactive Uc- or Yp-event is
381  * events lead to the Uc- or Yp-error state in the result.
382  * For each Up-event, a transition to a second error state, and
383  * for each Yp-event, a transition from the second to the first
384  * error state is inserted to realise the error behaviour.
385  * Note: states with NO active Uc- or Yp-event are ignored.
386  *
387  * @param rController
388  * HioController
389  * @param rResController
390  * reference to extended HioController (result)
391  *
392  * @ingroup hiosysplugin
393  *
394  */
395 extern FAUDES_API void HioFreeInput(
396  const HioController& rController,
397  HioController& rResController);
398 
399 /**
400  * HioFreeInput: extend HioEnvironment by obviously missing
401  * input transitions. States of the HioEnvironment in which a
402  * strict but nonempty subset of the Ul- or Ye-alphabet is active
403  * are extended by transitions to an error state such that
404  * now the whole Ul- or Ye-alphabet is active in that state.To
405  * avoid an additional deadlock violating completeness, an error
406  * behaviour (Ue Ye)* is concatenated to the error state
407  * using a second error state.
408  * Note that this method only helps making the input free in an
409  * hio system but does not guarantee a free input.
410  * Method: the transition relation of all states with at least
411  * one active AND at least one inactive Ul- or Ye-event is
412  * events lead to the Ul- or Ye-error state in the result.
413  * For each Ue-event, a transition to a second error state, and
414  * for each Ye-event, a transition from the second to the first
415  * error state is inserted to realise the error behaviour.
416  * Note: states with NO active Ul- or Ye-event are ignored.
417  *
418  * @param rEnvironment
419  * HioEnvironment
420  * @param rResEnvironment
421  * reference to extended HioEnvironment (result)
422  *
423  * @ingroup hiosysplugin
424  *
425  */
426 extern FAUDES_API void HioFreeInput(
427  const HioEnvironment& rEnvironment,
428  HioEnvironment& rResEnvironment);
429 
430 /**
431  * HioFreeInput: extend HioConstraint by obviously missing
432  * input transitions. States of the HioConstraint in which a
433  * strict but nonempty subset of the U-alphabet is active
434  * are extended by transitions to an error state such that
435  * now the whole U-alphabet is active in that state.To
436  * avoid an additional deadlock violating completeness, an error
437  * behaviour (U Y)* is concatenated to the error state
438  * using a second error state.
439  * Note that this method only helps making the input free in an
440  * hio system but does not guarantee a free input.
441  * Method: the transition relation of all states with at least
442  * one active AND at least one inactive U-event is
443  * events lead to the U-error state in the result.
444  * For each U-event, a transition to a second error state, and
445  * for each Y-event, a transition from the second to the first
446  * error state is inserted to realise the error behaviour.
447  * Note: states with NO active U-event are ignored.
448  *
449  * @param rConstraint
450  * HioConstraint
451  * @param rResConstraint
452  * reference to extended HioConstraint (result)
453  *
454  * @ingroup hiosysplugin
455  *
456  */
457 extern FAUDES_API void HioFreeInput(
458  const HioConstraint& rConstraint,
459  HioConstraint& rResConstraint);
460 
461 /**
462  * HioFreeInput: convenience interface to faudes::HioFreeInput(const HioPlant&, HioPlant)
463  *
464  * @param rPlant
465  * HioPlant
466  * @ingroup hiosysplugin
467  *
468  */
469 extern FAUDES_API void HioFreeInput(HioPlant& rPlant);
470 
471 /**
472  * HioFreeInput: convenience interface to faudes::HioFreeInput(const HioController&, HioController)
473  *
474  * @param rController
475  * HioController
476  * @ingroup hiosysplugin
477  *
478  */
479 extern FAUDES_API void HioFreeInput(HioController& rController);
480 
481 /**
482  * HioFreeInput: convenience interface to faudes::HioFreeInput(const HioEnvironment&, HioEnvironment)
483  *
484  * @param rEnvironment
485  * HioEnvironment
486  * @ingroup hiosysplugin
487  *
488  */
489 extern FAUDES_API void HioFreeInput(HioEnvironment& rEnvironment);
490 
491 /**
492  * HioFreeInput: convenience interface to faudes::HioFreeInput(const HioConstraint&, HioConstraint)
493  *
494  * @param rConstraint
495  * HioConstraint
496  * @ingroup hiosysplugin
497  *
498  */
499 extern FAUDES_API void HioFreeInput(HioConstraint& rConstraint);
500 
501 
502 //**********************************************************
503 //******************** IO-shuffle ************************
504 //**********************************************************
505 
506 /**
507  * MarkHioShuffle: marking rule for HioShuffle() in case of
508  * marked parameters rGen1 and rGen2 - UNDER CONSTRUCTION.
509  *
510  * Method:
511  * Strings ending with events from rGen1 are marked according
512  * to rGen1, strings ending with events from rGen2 are marked
513  * according to rGen2.
514  *
515  * @param rGen1
516  * First generator
517  * @param rGen2
518  * Second generator
519  * @param rReverseCompositionMap
520  * map from rGen1 and rGen2 state indeces to respective
521  * state indeces of result
522  * @param rShuffle
523  * Shuffle of rGen1 and rGen2 that shall receive marking
524  *
525  * @ingroup hiosysplugin
526  *
527  */
528 extern FAUDES_API void MarkHioShuffle(
529  const Generator& rGen1,
530  const Generator& rGen2,
531  const std::map< std::pair<Idx,Idx>, Idx >& rReverseCompositionMap,
532  Generator& rShuffle);
533 
534 /**
535  * CheapAltAnB: returns Generator of the following
536  * specification: "After a maximum of n (=depth) pairs of
537  * A-transitions, a B-transition has to occur!".
538  *
539  * @param rAset
540  * alphabet A
541  * @param rBset
542  * alphabet B
543  * @param Depth
544  * depth of alternation
545  * @param rAltAnB
546  * generator of AnB-specification
547  *
548  * @exception Exception
549  * - n less than 1 (id 0)
550  * - rAset empty (id 0)
551  * - rBset empty (id 0)
552  *
553  * @ingroup hiosysplugin
554  *
555  */
556 extern FAUDES_API void CheapAltAnB(
557  const EventSet rAset,
558  const EventSet rBset,
559  const int Depth,
560  Generator& rAltAnB);
561 
562 /**
563  * CheapAltAB: returns Generator of the following
564  * specification: "After a maximum of n (=depth) pairs of
565  * A-transitions, a B-transition has to occur and vice-versa!".
566  *
567  * @param rAset
568  * alphabet A
569  * @param rBset
570  * alphabet B
571  * @param Depth
572  * depth of alternation
573  * @param rAltAB
574  * generator of AB-specification
575  *
576  * @exception Exception
577  * - n less than 1 (id 0)
578  * - rAset empty (id 0)
579  * - rBset empty (id 0)
580  *
581  * @ingroup hiosysplugin
582  *
583  */
584 extern FAUDES_API void CheapAltAB(
585  const EventSet rAset,
586  const EventSet rBset,
587  const int Depth,
588  Generator& rAltAB);
589 
590 /**
591  * MarkAlternationAB: returns Generator marking the
592  * alternation of Aset-transitions with Bset-transitions.
593  * More docu will be provided soon.
594  *
595  * @param rAset
596  * alphabet A
597  * @param rBset
598  * alphabet B
599  * @param rAltAB
600  * recognizer of AB-alternation
601  *
602  * @exception Exception
603  * - rAset empty (id 0)
604  * - rBset empty (id 0)
605  *
606  * @ingroup hiosysplugin
607  *
608  */
609 extern FAUDES_API void MarkAlternationAB(
610  const EventSet rAset,
611  const EventSet rBset,
612  Generator& rAltAB);
613 
614 /**
615  * HioShuffleUnchecked: IO-shuffle of rPlantA and rPlantB
616  * according to definition, no parameter check. Moreover: marking
617  * of alternation according to MarkAlternationAB().
618  *
619  * TODO: 'checked' version
620  *
621  * @param rPlantA
622  * plant A generator
623  * @param rPlantB
624  * plant B generator
625  * @param rYp
626  * alphabet Yp
627  * @param rUp
628  * alphabet Up
629  * @param rYe
630  * alphabet Ye
631  * @param rUe
632  * alphabet Ue
633  * @param rIOShuffAB
634  * reference to I/O-shuffle generator
635  *
636  * @ingroup hiosysplugin
637  *
638  */
639 extern FAUDES_API void HioShuffleUnchecked(
640  const Generator& rPlantA,
641  const Generator& rPlantB,
642  const EventSet& rYp,
643  const EventSet& rUp,
644  const EventSet& rYe,
645  const EventSet& rUe,
646  Generator& rIOShuffAB);
647 
648 /**
649  * HioShuffle: IO-shuffle of rPlantA and rPlantB according
650  * to definition. Moreover: marking of alternation
651  * according to MarkAlternationAB().
652  *
653  *
654  * @param rPlantA
655  * plant A generator
656  * @param rPlantB
657  * plant B generator
658  * @param rYp
659  * alphabet Yp
660  * @param rUp
661  * alphabet Up
662  * @param rYe
663  * alphabet Ye
664  * @param rUe
665  * alphabet Ue
666  * @param rIOShuffAB
667  * reference to I/O-shuffle generator
668  *
669  * @exception Exception
670  * - empty or non-disjoint alphabets rYp, rUp, rYe, rUe (id 0).
671  * - plant A or plant B not in HioPlantForm (id 0).
672  *
673  * @ingroup hiosysplugin
674  *
675  */
676 extern FAUDES_API void HioShuffle(
677  const Generator& rPlantA,
678  const Generator& rPlantB,
679  const EventSet& rYp,
680  const EventSet& rUp,
681  const EventSet& rYe,
682  const EventSet& rUe,
683  Generator& rIOShuffAB);
684 
685 /**
686  * HioShuffle: IO-shuffle of rPlantA and rPlantB according
687  * to definition. Moreover: alternation of depth
688  * Depth (see CheapAltAB()) between A- and B-events (no
689  * alternation for Depth=1) and marking of alternation
690  * according to MarkAlternationAB().
691  *
692  * @param rPlantA
693  * HioPlant A
694  * @param rPlantB
695  * HioPlant B
696  * @param rIOShuffAB
697  * reference to composed HioPlant
698  *
699  * @exception Exception
700  * - todo...
701  *
702  * @ingroup hiosysplugin
703  *
704  */
705 extern FAUDES_API void HioShuffle(
706  const HioPlant& rPlantA,
707  const HioPlant& rPlantB,
708  HioPlant& rIOShuffAB);
709 
710 //******************** old version: no marking, forced alternation ************************
711 /**
712  * HioShuffleTU: IO-shuffle of rPlantA and rPlantB according
713  * to definition with additional forced alternation of depth
714  * Depth (see CheapAltAB()) between A- and B-events.
715  * -> frozen version for transport unit example
716  *
717  * @param rPlantA
718  * plant A generator
719  * @param rPlantB
720  * plant B generator
721  * @param rYp
722  * alphabet Yp
723  * @param rUp
724  * alphabet Up
725  * @param rYe
726  * alphabet Ye
727  * @param rUe
728  * alphabet Ue
729  * @param Depth
730  * depth of alternation
731  * @param rIOShuffAB
732  * reference to I/O-shuffle generator
733  *
734  * @exception Exception
735  * - todo...
736  *
737  * @ingroup hiosysplugin
738  *
739  */
740 extern FAUDES_API void HioShuffleTU(
741  const Generator& rPlantA,
742  const Generator& rPlantB,
743  const EventSet& rYp,
744  const EventSet& rUp,
745  const EventSet& rYe,
746  const EventSet& rUe,
747  const int Depth,
748  Generator& rIOShuffAB);
749 
750 //**********************************************************
751 //******************** Cycles ************************
752 //**********************************************************
753 
754 /**
755  * SearchYclessSCC: Search for strongly connected ycless
756  * components (YC-less SCC's). This function partitions the
757  * stateset of a generator into equivalent classes such that
758  * states x1 and x2 are equivalent iff there is a ycless
759  * path from x1 to x2 and a ycless path from x2 to x1.
760  * "Trivial" SCC's consisting of one state without non-Yc-
761  * selfloop are omitted, SCC's consisting exclusively of
762  * unmarked states are stored in rUnMarkedSccSet; all OTHER
763  * SCC's are collected in rSccSet. Their roots (i.e. that
764  * state of each SCC that has been visited first during depth
765  * first search of the generator) are collected in rRoots.
766  * This function is built on the algorithm based on a depth
767  * first search presented in:
768  * "Aho, Hopcroft, Ullman:
769  * The Design and Analysis of Computer Algorithms"
770  * Most of the comments in this function have been literally
771  * taken from this book!
772  * An api with generator and Yc-events as input parameters
773  * and the set of YC-less SCC's as output parameters is
774  * provided right below this method.
775  *
776  * @param state
777  * State, from which the current recursion is started.
778  * @param rcount
779  * Denotes the current depth of the recursion.
780  * @param rGen
781  * investigated generator
782  * @param rYc
783  * alphabet Yc
784  * @param UnMarkedOnly
785  * if set true, being unmarked is an additional condition for equivalence of states
786  * @param rNewStates
787  * Set of states that up to now were not found by the
788  * depth first search.
789  * @param rSTACK
790  * Stack of state indeces.
791  * @param rStackStates
792  * Set of states whose indeces are on STACK.
793  * @param rDFN
794  * Map assigning to each state idx its Depth-First Number.
795  * @param rLOWLINK
796  * Map assigning to each state its LOWLINK Number.
797  * @param rSccSet
798  * Set of YC-less strongly connected components (result).
799  * @param rRoots
800  * Set of states that each are root of some SCC (result).
801  *
802  * @exception Exception
803  * - todo...
804  *
805  * @ingroup hiosysplugin
806  *
807  */
808 extern FAUDES_API void SearchYclessScc(
809  const Idx state,
810  int& rcount, // why is this a ref?
811  const Generator& rGen,
812  const EventSet& rYc,
813  const bool UnMarkedOnly,
814  StateSet& rNewStates,
815  std::stack<Idx>& rSTACK,
816  StateSet& rStackStates,
817  std::map<const Idx, int>& rDFN,
818  std::map<const Idx, int>& rLOWLINK,
819  std::set<StateSet>& rSccSet,
820  StateSet& rRoots);
821 
822 /**
823  * YclessSCC: Search for strongly connected ycless
824  * components (YC-less SCC's) - convenience api. See
825  * SearchYclessSCC() for docu.
826  *
827  * @param rGen
828  * investigated generator
829  * @param rYc
830  * alphabet Yc
831  * @param rSccSet
832  * Set of YC-less strongly connected components (result).
833  * @param rRoots
834  * Set of states that each are root of some SCC (result).
835  *
836  * @return
837  * true if YclessSCC's have been found, false if not.
838  *
839  * @exception Exception
840  * - todo...
841  *
842  * @ingroup hiosysplugin
843  *
844  */
845 extern FAUDES_API bool YclessScc(
846  const Generator& rGen,
847  const EventSet& rYc,
848  std::set<StateSet>& rSccSet,
849  StateSet& rRoots);
850 
851 
852 /**
853  * YclessUnmarkedSCC: Search for strongly connected ycless
854  * components (YC-less SCC's) consisting of unmarked states only.
855  * Uses SearchYclessSCC().
856  *
857  * @param rGen
858  * investigated generator
859  * @param rYc
860  * alphabet Yc
861  * @param rSccSet
862  * Set of unmarked YC-less strongly connected components (result).
863  * @param rRoots
864  * Set of states that each are root of some SCC (result).
865  *
866  * @return
867  * true if unmarked YclessSCC's have been found, false if not.
868  *
869  * @exception Exception
870  * - todo...
871  *
872  * @ingroup hiosysplugin
873  *
874  */
875 extern FAUDES_API bool YclessUnmarkedScc(
876  const Generator& rGen,
877  const EventSet& rYc,
878  std::set<StateSet>& rSccSet,
879  StateSet& rRoots);
880 
881 /**
882  * YclessSCC: Search for strongly connected ycless
883  * components (YC-less SCC's) - convenience api. See
884  * SearchYclessSCC() for docu.
885  *
886  * @param rGen
887  * investigated generator
888  * @param rYc
889  * alphabet Yc
890  * @param rSccSet
891  * Set of YC-less strongly connected components (result).
892  *
893  * @return
894  * true if YclessSCC's have been found, false if not.
895  *
896  * @exception Exception
897  * - todo...
898  *
899  * @ingroup hiosysplugin
900  *
901  */
902 extern FAUDES_API bool YclessSCC(
903  const Generator& rGen,
904  const EventSet& rYc,
905  std::set<StateSet>& rSccSet);
906 
907 /**
908  * IsYcLive: This function checks if generator is Yc-live.
909  * Method: using YclessSCC(), the function checks if no Yc-less
910  * SCC is found.
911  *
912  * @param rGen
913  * investigated generator
914  * @param rYc
915  * alphabet Yc
916  *
917  * @return
918  * true if Generator is YcLive.
919  *
920  * @exception Exception
921  * - todo...
922  *
923  * @ingroup hiosysplugin
924  *
925  */
926 extern FAUDES_API bool IsYcLive(
927  const Generator& rGen,
928  const EventSet& rYc);
929 
930 /**
931  * WriteStateSets: Write set of StateSet's to console (indeces).
932  * Useful to output partitions over statesets like e.g. the
933  * set of strongly connected components. Also serves as
934  * template for walkthrough through each state of a set of
935  * statesets.
936  *
937  * @param rStateSets
938  * Reference to set of StateSets (result).
939  *
940  * @exception Exception
941  * - todo?
942  *
943  * @ingroup hiosysplugin
944  *
945  */
946 extern FAUDES_API void WriteStateSets(
947  const std::set<StateSet>& rStateSets);
948 
949 /**
950  * WriteStateSets: Write set of StateSet's to console (symbolic
951  * state names taken from rGen).
952  * Useful to output partitions over statesets like e.g. the
953  * set of strongly connected components. Also serves as
954  * template for walkthrough through each state of a set of
955  * statesets.
956  *
957  * @param rGen
958  * Generator holding symbolic state names.
959  * @param rStateSets
960  * Reference to set of StateSets (result).
961  *
962  * @exception Exception
963  * - todo?
964  *
965  * @ingroup hiosysplugin
966  *
967  */
968 extern FAUDES_API void WriteStateSets(
969  const Generator& rGen,
970  const std::set<StateSet>& rStateSets);
971 
972 /**
973  * SCCEntries: figure entry states and entry transitions of
974  * strongly connected components rSccSet of rGen. Entry
975  * states are the set of states of the SCC that are initial
976  * state or direct successor of some state not belonging to
977  * this SCC (i.e. belonging to a different or no SCC). Entry
978  * transitions are the set of respective transitions leading
979  * to an entrystate of some SCC from a state not belonging
980  * to this SCC.
981  *
982  * @param rGen
983  * generator holding SCC's of rSccSet
984  * @param rSccSet
985  * generator holding SCC's of rSccSet
986  * @param rEntryStates
987  * reference to set of entry states of all SCC's (result)
988  * @param rEntryTransSet
989  * reference to set of entry transitions, sorted by X2
990  * (result)
991  *
992  * @exception Exception
993  * - todo: if FAUDES_CHECKED: check if elements of rSccSet
994  * are all subsets of StateSet of rGen.
995  *
996  * @ingroup hiosysplugin
997  *
998  */
999 extern FAUDES_API void SccEntries(
1000  const Generator& rGen,
1001  const std::set<StateSet>& rSccSet,
1002  StateSet& rEntryStates,
1003  TransSetX2EvX1& rEntryTransSet);
1004 
1005 /**
1006  * cloneSCC: makes a copy (clone) of strongly connected
1007  * component (rSCC) of the generator and moves all
1008  * transitions leading to some entry state EntryState of
1009  * this SCC to the copy of EntryState. If this is carried
1010  * out for n-1 of all n entry states of the SCC, then, in
1011  * the generator, this one SCC is transformed into n SCC's
1012  * with one unique entry state each.
1013  * The set of SCC's is extended by the clone-SCC. The set of
1014  * entry states is extended by the (unique) entry state of
1015  * the clone-SCC.
1016  * Note: all added states are equivalent to some state in
1017  * the original generator, the behaviour is not changed.
1018  * The basic idea of this algorithm id taken from
1019  * [Jéron,Marchand,Rusu,Tschaen] "Ensuring the conformance
1020  * of reactive discrete-event systems using supervisory
1021  * control" (CDC'03)
1022  * todo: check const parameters
1023  *
1024  * @param rGen
1025  * generator holding SCC's of rSccSet
1026  * @param rScc
1027  * SCC of rGen that is to be cloned // Perk: check if idx of rSccSet is better?
1028  * @param rSccSet
1029  * set of all SCC's of rGen
1030  * @param EntryState
1031  * one of the entry states of this SCC
1032  * @param rEntryStates
1033  * set of entry states of this SCC
1034  * @param rEntryTransSet
1035  * set of respective transitions to the entry states,
1036  * sorted by X2
1037  *
1038  * @exception Exception
1039  * - todo: exceptions, e.g. for rEntryState not subset of
1040  * rEntryStates not subset of rScc not element of rSccSet,
1041  * elements of rSccSet not subset of rGen.States() etc.
1042  *
1043  * @ingroup hiosysplugin
1044  *
1045  */
1046 
1047 extern FAUDES_API void CloneScc(
1048  Generator& rGen,
1049  const StateSet& rScc,
1050  std::set<StateSet>& rSccSet,
1051  const Idx EntryState,
1052  StateSet& rEntryStates,
1053  TransSetX2EvX1& rEntryTransSet);
1054 
1055 /**
1056  * CloneUnMarkedSCC: makes a copy (clone) of strongly connected
1057  * unmarked component (rSCC) of rGen.
1058  *
1059  * @ingroup hiosysplugin
1060 */
1061 
1062 extern FAUDES_API void CloneUnMarkedScc(
1063  Generator& rGen,
1064  const StateSet& rScc,
1065  const Idx EntryState,
1066  const StateSet& rEntryStates,
1067  TransSetX2EvX1& rEntryTransSet);
1068 
1069 /**
1070  * YcAcyclic: Computes the supremal(?) Yc-acyclic
1071  * sublanguage of L(Gen). Procedure:
1072  * 1) Find Yc-less SCC's with YclessScc(...)
1073  * 2) transform SCC's with n entry states to n SCC's with
1074  * one unique entry state.
1075  * 3) erase transitions leading from a state of some SCC to
1076  * the entry state of this SCC's.
1077  * 4) repeat 1)-3) until no more Yc-less SCC is found, i.e.
1078  * rResGen generates the supremal YcAcyclic sublanguage of
1079  * the language generated by rGen.
1080  *
1081  * @param rGen
1082  * input generator
1083  * @param rYc
1084  * alphabet Yc
1085  * @param rResGen
1086  * generator of supremal YcAcyclic sublanguage
1087  *
1088  * @exception Exception
1089  * - todo: rYc must be subset of rGen.Alphabet()
1090  *
1091  * @ingroup hiosysplugin
1092  *
1093 */
1094 extern FAUDES_API void YcAcyclic(
1095  const Generator& rGen,
1096  const EventSet& rYc,
1097  Generator& rResGen);
1098 
1099 //**********************************************************
1100 //******************** hio synthesis ************************
1101 //**********************************************************
1102 
1103 /**
1104  * ConstrSynth_Beta: compute operator constraint Sp for plant under
1105  * environment constraint Sl such that plant is complete & Yp-live wrt
1106 * both constraints - Beta Version. Plant can be individual or
1107  * composed, ie Plant=Lpe || Le, or Plant=Lpe1 ||io Lpe2 || Lel || Ll,
1108  * ie composition of plant and envconstr, or composition of HioShuffle
1109  * of two plants with environment and envconstr.
1110  * Parameter rLocConstr is optional and may contain environment
1111  * constraints for Lpe1 and Lpe2; rOpConstraint is computed such that
1112  * rLocConstr is met under rOpConstraint.
1113  * More and better docu will follow in future version.
1114  *
1115  * @param rPlant
1116  * model of plant under environment constraint.
1117  * @param rYp
1118  * alphabet YP
1119  * @param rUp
1120  * alphabet UP
1121  * @param rLocConstr
1122  * reference to optional local constraints
1123  * @param rOpConstraint
1124  * reference to operator constraint
1125  *
1126  * @ingroup hiosysplugin
1127  *
1128 */
1129 extern FAUDES_API void ConstrSynth_Beta(
1130  Generator& rPlant,
1131  const EventSet& rYp,
1132  const EventSet& rUp,
1133  const Generator& rLocConstr,
1134  Generator& rOpConstraint);
1135 
1136 /**
1137  * HioSynthUnchecked: I/O controller synthesis procedure, no
1138  * parameter check. Main hio synthesis algorithm suitable for both
1139  * the monolithic and the hierarchical case, see also respective api's
1140  * HioSynth(with parameter check), HioSynthMonolithic and
1141  * HioSynthHierarchical. The result rController realises a solution to
1142  * the I/O controller synthesis problem (S_PE,S_C,S_P,S_E,S_SpecCE).
1143  *
1144  * @param rPlant
1145  * plant model generator:
1146  * - monolithic case: I/O plant to be controlled;
1147  * - hierarchical case: parallel composition of group
1148  * (I/O-shuffle) of n I/O plants S_PEi (or their
1149  * abstractions) with the environment model S_EL for
1150  * this group.
1151  * @param rSpec
1152  * generator of desired behaviour of the external closed
1153  * loop over alphabet SigmaCE. Must be in I/O plant form.
1154  * @param rConstr
1155  * external constraint that may be assumed:
1156  * - monolithic case: composition of constraints S_C and
1157  * S_E
1158  * - hierarchical case: composition of constraints S_C and
1159  * S_L
1160  * @param rLocConstr
1161  * internal constraint that has to be achieved by the I/O
1162  * controller for the closed loop:
1163  * - monolithic case: generator of constraint S_P
1164  * - hierarchical case: parallel composition of
1165  * constraints S_Pi and S_Ei
1166  * @param rYc
1167  * alphabet YC
1168  * @param rUc
1169  * alphabet UC
1170  * @param rYp
1171  * alphabet YP
1172  * @param rUp
1173  * alphabet UP
1174  * @param rYel
1175  * monolithic: alphabet YE, hierarchical: alphabet YL
1176  * @param rUel
1177  * monolithic: alphabet UE, hierarchical: alphabet UL
1178  * @param rController
1179  * reference to I/O controller(result)
1180  *
1181  * @ingroup hiosysplugin
1182  *
1183 */
1184 extern FAUDES_API void HioSynthUnchecked(
1185  const Generator& rPlant,
1186  const Generator& rSpec,
1187  const Generator& rConstr,
1188  const Generator& rLocConstr,
1189  const EventSet& rYc,
1190  const EventSet& rUc,
1191  const EventSet& rYp,
1192  const EventSet& rUp,
1193  const EventSet& rYel,
1194  const EventSet& rUel,
1195  Generator& rController);
1196 
1197 /**
1198  * HioSynthUnchecked: I/O controller synthesis procedure.
1199  * Main hio synthesis algorithm suitable for both
1200  * the monolithic and the hierarchical case, see also respective api's
1201  * HioSynthMonolithic and HioSynthHierarchical.
1202  * The result rController realises a solution to the I/O controller
1203  * synthesis problem (S_PE,S_C,S_P,S_E,S_SpecCE).
1204  *
1205  * @param rPlant
1206  * plant model generator:
1207  * - monolithic case: I/O plant to be controlled;
1208  * - hierarchical case: parallel composition of group
1209  * (I/O-shuffle) of n I/O plants S_PEi (or their
1210  * abstractions) with the environment model S_EL for
1211  * this group.
1212  * @param rSpec
1213  * generator of desired behaviour of the external closed
1214  * loop. Must be in I/O plant form.
1215  * @param rConstr
1216  * external constraint that may be assumed:
1217  * - monolithic case: composition of constraints S_C and
1218  * S_E
1219  * - hierarchical case: composition of constraints S_C and
1220  * S_L
1221  * @param rLocConstr
1222  * internal constraint that has to be achieved by the I/O
1223  * controller for the closed loop:
1224  * - monolithic case: generator of constraint S_P
1225  * - hierarchical case: parallel composition of
1226  * constraints S_Pi and S_Ei
1227  * @param rYc
1228  * alphabet YC
1229  * @param rUc
1230  * alphabet UC
1231  * @param rYp
1232  * alphabet YP
1233  * @param rUp
1234  * alphabet UP
1235  * @param rYel
1236  * monolithic: alphabet YE, hierarchical: alphabet YL
1237  * @param rUel
1238  * monolithic: alphabet UE, hierarchical: alphabet UL
1239  * @param rController
1240  * reference to I/O controller(result)
1241  *
1242  * @exception Exception
1243  * - empty or non-disjoint alphabets rYc, rUc, rYp, rUp, rYel, rUel (id 0).
1244  * - rSpec not in HioPlantForm (id 0).
1245  * - alphabet mismatch between plant or constraints and spec (id 0).
1246  *
1247  * @ingroup hiosysplugin
1248  *
1249 */
1250 extern FAUDES_API void HioSynth(
1251  const Generator& rPlant,
1252  const Generator& rSpec,
1253  const Generator& rConstr,
1254  const Generator& rLocConstr,
1255  const EventSet& rYc,
1256  const EventSet& rUc,
1257  const EventSet& rYp,
1258  const EventSet& rUp,
1259  const EventSet& rYel,
1260  const EventSet& rUel,
1261  Generator& rController);
1262 
1263 /**
1264  * HioSynthMonolithic: I/O controller synthesis procedure for
1265  * monolithic plant. The result rController realises a solution to
1266  * the I/O controller synthesis problem (S_PE,S_C,S_P,S_E,S_SpecCE).
1267  *
1268  * @param rPlant
1269  * I/O plant to be controlled; must be in I/O plant form (tested if
1270  * FAUDES_CHECKED); must be complete and Yp-live wrt. Sp and
1271  * Se (not tested).
1272  * @param rSpec
1273  * I/O plant model of desired behaviour of the external closed
1274  * loop. Must be in I/O plant form (tested if FAUDES_CHECKED);
1275  * must be complete and Yp-live wrt. Sc and Se (not tested).
1276  * @param rSc
1277  * external operator constraint that may be assumed; I/O constraint form
1278  * is recommended.
1279  * @param rSp
1280  * operator constraint for rPlant; is met by admissibility of rController;
1281  * I/O constraint form is recommended.
1282  * @param rSe
1283  * environment constraint that may be assumed; I/O constraint form
1284  * is recommended.
1285  * @param rController
1286  * I/O controller solving the I/O controller synthesis problem (result)
1287  *
1288  * @exception Exception
1289  * - plant or spec not in HioPlantForm (id 0).
1290  * - alphabet mismatch between plant or constraints and spec (id 0).
1291  *
1292  * @ingroup hiosysplugin
1293  *
1294 */
1295 extern FAUDES_API void HioSynthMonolithic(
1296  const HioPlant& rPlant,
1297  const HioPlant& rSpec,
1298  const HioConstraint& rSc,
1299  const HioConstraint& rSp,
1300  const HioConstraint& rSe,
1301  HioController& rController);
1302 
1303 /**
1304  * HioSynthHierarchical: I/O controller synthesis procedure for
1305  * I/O-shuffle of i plants and their interaction via an I/O environment.
1306  * The result rController realises a solution to the I/O controller
1307  * synthesis problem (S_PE,S_C,S_P,S_E,S_SpecCE) with the external
1308  * behaviour S_PE of the I/Oshuffle-environment-composition and respects
1309  * internal constraints Sp_i and Se_i preserving liveness of the
1310  * individual plants.
1311  *
1312  * @param rHioShuffle
1313  * I/O plant or group of I/O plants composed by I/O shuffle
1314  * @param rEnvironment
1315  * environment model for rHioShuffle
1316  * @param rSpec
1317  * I/O plant model of desired behaviour of the external closed
1318  * loop. Must be in I/O plant form (tested if FAUDES_CHECKED);
1319  * must be complete and Yp-live wrt. Sc and Se (not tested).
1320  * @param rIntConstr
1321  * parallel composition of constraints Sp_i and Se_i of the
1322  * individual plants composed to rHioShuffle
1323  * @param rSc
1324  * external operator constraint that may be assumed; I/O constraint form
1325  * is recommended.
1326  * @param rSl
1327  * environment constraint that may be assumed; I/O constraint form
1328  * is recommended.
1329  * @param rController
1330  * I/O controller solving the I/O controller synthesis problem (result)
1331  *
1332  * @exception Exception
1333  * - HioShuffle or spec not in HioPlantForm (id 0).
1334  * - Environment not in HioEnvironmentForm (id 0).
1335  * - alphabet mismatch between plant, environment, spec and constraints (id 0).
1336  *
1337  * @ingroup hiosysplugin
1338  *
1339 */
1340 extern FAUDES_API void HioSynthHierarchical(
1341  const HioPlant& rHioShuffle,
1342  const HioEnvironment& rEnvironment,
1343  const HioPlant& rSpec,
1344  const Generator& rIntConstr,
1345  const HioConstraint& rSc,
1346  const HioConstraint& rSl,
1347  HioController& rController);
1348 
1349 //#####################################
1350 // #### end of hio_functions - below just archive ########
1351 //#####################################
1352 
1353 //HioShuffle_Musunoi() - special version for HioModule. Will be changed to std HioShuffle.
1354 void HioShuffle_Musunoi(
1355  const HioPlant& rPlantA,
1356  const HioPlant& rPlantB,
1357  int depth,
1358  Generator& rIOShuffAB) ;
1359 
1360 //HioSynth_Musunoi() - special version for HioModule. Will be changed to std HioSynth.
1361 void HioSynth_Musunoi(
1362  const Generator& rPlant,
1363  const HioPlant& rSpec,
1364  const Generator& rConstr,
1365  const Generator& rLocConstr,
1366  const EventSet& rYp,
1367  const EventSet& rUp,
1368  Generator& rController);
1369 }
1370 
1371 
1372 #endif
#define FAUDES_API
Interface export/import symbols: windows.
Definition: cfl_platform.h:81
Set of indices.
Definition: cfl_indexset.h:78
Set of indices with symbolic names.
Definition: cfl_nameset.h:69
Set of Transitions.
Definition: cfl_transset.h:242
Base class of all FAUDES generators.
Includes all libFAUDES headers, no plugins.
IndexSet StateSet
Definition: cfl_indexset.h:271
NameSet EventSet
Convenience typedef for plain event sets.
Definition: cfl_nameset.h:531
vGenerator Generator
Plain generator, api typedef for generator with no attributes.
void CheapAltAnB(const EventSet rAset, const EventSet rBset, const int Depth, Generator &rAltAnB)
CheapAltAnB: returns Generator of the following specification: "After a maximum of n (=depth) pairs o...
void CloneScc(Generator &rGen, const StateSet &rScc, std::set< StateSet > &rSccSet, const Idx EntryState, StateSet &rEntryStates, TransSetX2EvX1 &rEntryTransSet)
cloneSCC: makes a copy (clone) of strongly connected component (rSCC) of the generator and moves all ...
void HioSynthUnchecked(const Generator &rPlant, const Generator &rSpec, const Generator &rExtConstr, const Generator &rLocConstr, const EventSet &rYc, const EventSet &rUc, const EventSet &rYp, const EventSet &rUp, const EventSet &rYel, const EventSet &rUel, Generator &rController)
HioSynthUnchecked: I/O controller synthesis procedure, no parameter check.
void ConstrSynth_Beta(Generator &rPlant, const EventSet &rYp, const EventSet &rUp, const Generator &rLocConstr, Generator &rOpConstraint)
ConstrSynth_Beta: compute operator constraint Sp for plant under environment constraint Sl such that ...
void HioSynth(const Generator &rPlant, const Generator &rSpec, const Generator &rExtConstr, const Generator &rLocConstr, const EventSet &rYc, const EventSet &rUc, const EventSet &rYp, const EventSet &rUp, const EventSet &rYel, const EventSet &rUel, Generator &rController)
HioSynthUnchecked: I/O controller synthesis procedure.
void HioShuffleTU(const Generator &rPlantA, const Generator &rPlantB, const EventSet &rUp, const EventSet &rYp, const EventSet &rYe, const EventSet &rUe, const int Depth, Generator &rIOShuffAB)
HioShuffleTU: IO-shuffle of rPlantA and rPlantB according to definition with additional forced altern...
void MarkAlternationAB(const EventSet rAset, const EventSet rBset, Generator &rAltAB)
MarkAlternationAB: returns Generator marking the alternation of Aset-transitions with Bset-transition...
void HioSynthMonolithic(const HioPlant &rPlant, const HioPlant &rSpec, const HioConstraint &rSc, const HioConstraint &rSp, const HioConstraint &rSe, HioController &rController)
HioSynthMonolithic: I/O controller synthesis procedure for monolithic plant.
void SearchYclessScc(const Idx state, int &rcount, const Generator &rGen, const EventSet &rYc, const bool UnMarkedOnly, StateSet &rNewStates, std::stack< Idx > &rSTACK, StateSet &rStackStates, std::map< const Idx, int > &rDFN, std::map< const Idx, int > &rLOWLINK, std::set< StateSet > &rSccSet, StateSet &rRoots)
SearchYclessSCC: Search for strongly connected ycless components (YC-less SCC's).
void HioFreeInput(const Generator &rGen, const EventSet &rInput, const EventSet &rOutput, Generator &rResGen, const std::string &rErrState1, const std::string &rErrState2, Idx &rErrState1Idx, Idx &rErrState2Idx)
HioFreeInput: extend generator by obviously missing input transitions.
void CheapAltAB(const EventSet rAset, const EventSet rBset, const int Depth, Generator &rAltAB)
CheapAltAB: returns Generator of the following specification: "After a maximum of n (=depth) pairs of...
void WriteStateSets(const std::set< StateSet > &rStateSets)
WriteStateSets: Write set of StateSet's to console (indeces).
FAUDES_API bool YclessSCC(const Generator &rGen, const EventSet &rYc, std::set< StateSet > &rSccSet)
YclessSCC: Search for strongly connected ycless components (YC-less SCC's) - convenience api.
Generator HioSortCL(const EventSet &rYc, const EventSet &rUc, const EventSet &rYp, const EventSet &rUp, const EventSet &rYe, const EventSet &rUe)
IoSortCL: returns IO-sorting structure required for closed loops.
void SccEntries(const Generator &rGen, const std::set< StateSet > &rSccSet, StateSet &rEntryStates, TransSetX2EvX1 &rEntryTransSet)
SCCEntries: figure entry states and entry transitions of strongly connected components rSccSet of rGe...
bool YclessUnmarkedScc(const Generator &rGen, const EventSet &rYc, std::set< StateSet > &rSccSet, StateSet &rRoots)
YclessUnmarkedSCC: Search for strongly connected ycless components (YC-less SCC's) consisting of unma...
void YcAcyclic(const Generator &rGen, const EventSet &rYc, Generator &rResGen)
YcAcyclic: Computes the supremal(?) Yc-acyclic sublanguage of L(Gen).
void CloneUnMarkedScc(Generator &rGen, const StateSet &rScc, const Idx EntryState, const StateSet &rEntryStates, TransSetX2EvX1 &rEntryTransSet)
CloneUnMarkedSCC: makes a copy (clone) of strongly connected unmarked component (rSCC) of rGen.
void HioShuffleUnchecked(const Generator &rPlantA, const Generator &rPlantB, const EventSet &rYp, const EventSet &rUp, const EventSet &rYe, const EventSet &rUe, Generator &rIOShuffAB)
HioShuffleUnchecked: IO-shuffle of rPlantA and rPlantB according to definition, no parameter check.
bool NormalCompleteSynthNB(Generator &rPlant, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rSpec, Generator &rClosedLoop)
NormalCompleteSynthNB: compute normal, complete, controllable and nonblocking sublanguage.
bool IsYcLive(const Generator &rGen, const EventSet &rYc)
IsYcLive: This function checks if generator is Yc-live.
bool NormalCompleteSynth(Generator &rPlant, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rSpec, Generator &rClosedLoop)
NormalCompleteSynth: compute normal, complete and controllable (and closed) sublanguage.
void HioSynthHierarchical(const HioPlant &rHioShuffle, const HioEnvironment &rEnvironment, const HioPlant &rSpec, const Generator &rIntConstr, const HioConstraint &rSc, const HioConstraint &rSl, HioController &rController)
HioSynthHierarchical: I/O controller synthesis procedure for I/O-shuffle of i plants and their intera...
void MarkHioShuffle(const Generator &rGen1, const Generator &rGen2, const std::map< std::pair< Idx, Idx >, Idx > &rMapOrigToResult, Generator &rShuffle)
MarkHioShuffle: marking rule for HioShuffle() in case of marked parameters rGen1 and rGen2 - UNDER CO...
bool CompleteSynth(const Generator &rPlant, const EventSet rCAlph, const Generator &rSpec, Generator &rClosedLoop)
CompleteSynth: compute supremal complete and controllable (and closed) sublanguage.
bool YclessScc(const Generator &rGen, const EventSet &rYc, std::set< StateSet > &rSccSet, StateSet &rRoots)
YclessSCC: Search for strongly connected ycless components (YC-less SCC's) - convenience api.
void HioShuffle(const Generator &rPlantA, const Generator &rPlantB, const EventSet &rYp, const EventSet &rUp, const EventSet &rYe, const EventSet &rUe, Generator &rIOShuffAB)
HioShuffle: IO-shuffle of rPlantA and rPlantB according to definition.
Generator with I/O-constraint attributes.
Generator with I/O-controller attributes.
Generator with I/O-environment attributes.
Generator with I/O-plant attributes.
libFAUDES resides within the namespace faudes.
uint32_t Idx
Type definition for index type (allways 32bit)
THioController< AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoid > HioController
THioConstraint< AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoid > HioConstraint
THioEnvironment< AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoid > HioEnvironment
THioPlant< AttributeVoid, HioStateFlags, HioEventFlags, AttributeVoid > HioPlant
Definition: hio_plant.h:880
void HioSynth_Musunoi(const Generator &rPlant, const HioPlant &rSpec, const Generator &rConstr, const Generator &rLocConstr, const EventSet &rYp, const EventSet &rUp, Generator &rController)
void HioShuffle_Musunoi(const HioPlant &rPlantA, const HioPlant &rPlantB, int depth, Generator &rIOShuffAB)

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