syn_supnorm.cpp
Go to the documentation of this file.
1 /** @file syn_supnorm.cpp Supremal normal 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_supnorm.h"
24 #include "syn_supcon.h"
25 
26 /* turn on debugging for this file */
27 //#undef FD_DF
28 //#define FD_DF(a) FD_WARN(a);
29 
30 namespace faudes {
31 
32 
33 
34 
35 /*
36 ***************************************************************************************
37 ***************************************************************************************
38  Implementation
39 ***************************************************************************************
40 ***************************************************************************************
41 */
42 
43 
44 //void NormalityConsistencyCheck(rL,rOAlph,rK)
46  const Generator& rL,
47  const EventSet& rOAlph,
48  const Generator& rK) {
49 
50  FD_DF("NormalityConsistencyCheck(...)");
51 
52  if(!(rK.IsDeterministic())) {
53  std::stringstream errstr;
54  errstr << "Nondeterministic parameter rK.";
55  if(!(rL.IsDeterministic())) errstr << "Nondeterministic parameter rL.";
56  throw Exception("NormalityConsistencyCheck", errstr.str(), 101);
57  }
58  if(!(rL.IsDeterministic())) {
59  std::stringstream errstr;
60  errstr << "Nondeterministic parameter rL.";
61  if(!(rL.IsDeterministic())) errstr << "Nondeterministic parameter rL.";
62  throw Exception("NormalityConsistencyCheck", errstr.str(), 101);
63  }
64 
65  EventSet Kevents,Sigma;
66  Sigma=rL.Alphabet();
67  Kevents=rK.Alphabet();
68 
69  // observable events have to be subset of Sigma
70  if(!(rOAlph<=Sigma)) {
71  EventSet only_in_OAlph = rOAlph - Sigma;
72  std::stringstream errstr;
73  errstr << "Not all observable events are contained in Sigma: "
74  << only_in_OAlph.ToString() << ".";
75  throw Exception("NormalityConsistencyCheck", errstr.str(), 100);
76  }
77 
78  // alphabets must match
79  if(Sigma != Kevents) {
80  EventSet only_in_L = Sigma - Kevents;
81  EventSet only_in_K = Kevents - Sigma;
82  only_in_L.Name("Only_In_L");
83  only_in_L.Name("Only_In_K");
84  std::stringstream errstr;
85  errstr << "Alphabets of generators do not match.";
86  if(!only_in_L.Empty())
87  errstr << " " << only_in_L.ToString() << ".";
88  if(!only_in_K.Empty())
89  errstr << " " << only_in_K.ToString() << ".";
90  throw Exception("NormalityConsistencyCheck", errstr.str(), 100);
91  }
92 
93  // K must be subset of L
94  if(!LanguageInclusion(rK,rL)) {
95  std::stringstream errstr;
96  errstr << "K is not subset of L.";
97  throw Exception("NormalityConsistencyCheck", errstr.str(), 0);
98  }
99 
100  FD_DF("NormalityConsistencyCheck(...): passed");
101 }
102 
103 // IsNormal(rK,rL,rOAlph)
104 bool IsNormal(
105  const Generator& rL,
106  const EventSet& rOAlph,
107  const Generator& rK)
108 {
109  FD_DF("IsNormal(...)");
110 
111  // bail out on empty K
112  // note: this is required to survive the
113  // determinism test when rK has no states at all
114  if(IsEmptyLanguage(rK)) return true;
115 
116  // determinism required
117  NormalityConsistencyCheck(rL,rOAlph,rK);
118 
119  //extract overall alphabet:
120  EventSet Sigma;
121  Sigma=rL.Alphabet();
122 
123  //extract alphabet of rK:
124  EventSet Kevents;
125  Kevents=rK.Alphabet();
126 
127  //calculate p(K)
128  Generator Ktest1, Ktest2;
129  Ktest1.StateNamesEnabled(false);
130  Ktest2.StateNamesEnabled(false);
131  Project(rK,rOAlph,Ktest1);
132 
133  //calculate pinv(p(K))
134  InvProject(Ktest1, Sigma);
135 
136  //check normality: pinv(p(K)) intersect L = K?
137  LanguageIntersection(Ktest1,rL,Ktest2);
138  return LanguageInclusion(Ktest2,rK);
139 
140  // Remark: testing for LanguageEquality is not required, as inclusion
141  // in the reverse direction is always met (assuming K\subseteq L)
142 }
143 
144 
145 
146 // IsNormal rti wrapper
147 bool IsNormal(const System& rPlantGen, const Generator& rSupCandGen) {
148  return IsNormal(rPlantGen, rPlantGen.ObservableEvents(),rSupCandGen);
149 }
150 
151 
152 // ConcatenateFullLanguage(rGen)
154  FD_DF("ConcatenateFullLanguage(" << rGen.Name() << ")");
155 
156  // prepare result
157  rGen.Name("ConcatenateFullLanguage(" + rGen.Name() + ")");
158 
159  // treat trivial empty result in case of empty marked language
160  if(rGen.MarkedStatesSize()==0) {
161  rGen.Clear();
162  return;
163  }
164 
165  // treat trivial case if marked initial state
166  if( ! (rGen.InitStates() * rGen.MarkedStates()).Empty() ) {
167  FD_DF("ConcatenateFullLanguage(...): marked initial state");
168  // reduce to empty string language
169  rGen.ClearStates();
170  rGen.ClearTransRel();
171  Idx state=rGen.InsInitState();
172  rGen.SetMarkedState(state);
173  // now concatenate Sigma* by selflooping marked state with all events
174  EventSet::Iterator eit;
175  for(eit = rGen.AlphabetBegin(); eit != rGen.AlphabetEnd(); ++eit)
176  rGen.SetTransition(state,*eit,state);
177  return;
178  }
179 
180  // helpers
181  EventSet alph=rGen.Alphabet();
182  StateSet StatesToClear;
183  TransSet TransToClear,TransToSet;
184  StateSet::Iterator sit;
185  TransSet::Iterator tit, tit_end;;
186  EventSet::Iterator eit;
187 
188 
189  // all marked states become eqivalent -> switch transitions leading to marked states to one remaining marked state
190  // and delete all the others
191  sit = rGen.MarkedStatesBegin();
192  Idx marked = *sit;
193  // clear all transitions the one marked states
194  tit = rGen.TransRelBegin(marked);
195  tit_end = rGen.TransRelEnd(marked);
196  while(tit != tit_end)
197  rGen.ClrTransition(tit++);
198  rGen.Accessible();
199  FD_DF("ConcatenateFullLanguage(...): cleared transitions");
200 
201 
202  // relink transitions to all other marked states if there are any
203  if(rGen.MarkedStatesSize()>1) {
204  // extract transitions sorted by target state X2
205  TransSetX2EvX1 trel;
206  rGen.TransRel(trel);
207  TransSetX2EvX1::Iterator tit2, tit2_end;
208  // switch transitions to all other marked states to the one remaining marked state
209  ++sit;
210  for(; sit != rGen.MarkedStatesEnd(); ++sit) {
211  tit2 = trel.BeginByX2(*sit);
212  tit2_end = trel.EndByX2(*sit);
213  for(; tit2 != tit2_end; ++tit2)
214  rGen.SetTransition(tit2->X1,tit2->Ev,marked);
215  }
216  FD_DF("ConcatenateFullLanguage(...): relinked transitions");
217  // delete all but the remaining marked state (note: by doing so, also corresp. transitions are cleared.)
218  sit = rGen.MarkedStatesBegin();
219  ++sit;
220  for(; sit != rGen.MarkedStatesEnd(); ++sit)
221  StatesToClear.Insert(*sit);
222  rGen.DelStates(StatesToClear);
223  FD_DF("ConcatenateFullLanguage(...): removed #" << StatesToClear.Size() << " marked states");
224  }
225  // now concatenate Sigma* by selflooping marked state with all events
226  for(eit = rGen.AlphabetBegin(); eit != rGen.AlphabetEnd(); ++eit)
227  rGen.SetTransition(marked,*eit,marked);
228 
229  FD_DF("ConcatenateFullLanguage(...): done");
230 }
231 
232 
233 // SupNorm(rL,rOAlph,rK,rResult)
234 bool SupNorm(
235  const Generator& rL,
236  const EventSet& rOAlph,
237  const Generator& rK,
238  Generator& rResult)
239 {
240  FD_DF("SupNorm(" << rL.Name() << "," << rK.Name() << "," << rOAlph.Name() << ")");
241  FD_DF("SupNorm: sizeof L, K: "<< rL.Size() << ", " << rK.Size());
242 
243  // exceprions
244  NormalityConsistencyCheck(rL,rOAlph,rK);
245 
246 
247  //extract overall alphabet:
248  EventSet allevents;
249  allevents=rL.Alphabet();
250 
251  // involved operations from cfl_regular.h operate on the marked
252  // languages -> turn generated languages into marked langusges
253  Generator prL=rL;
254  prL.InjectMarkedStates(rL.States());
255  Generator prK=rK;
256  prK.InjectMarkedStates(prK.States());
257 
258  // calculate "L-K"
259  rResult.StateNamesEnabled(false);
260  LanguageDifference(prL,prK,rResult);
261  FD_DF("SupNorm: sizeof L-K: "<< rResult.Size());
262 
263  // statmin before projection for performance (?)
264  //StateMin(rResult,rResult);
265  //FD_DF("SupNorm: sizeof statemin(L-K): "<< rResult.Size());
266 
267  // calculate Pinv(P(L-K)):
268  Project(rResult,rOAlph,rResult);
269  FD_DF("SupNorm: sizeof p(L-K): "<< rResult.Size());
270  InvProject(rResult,allevents);
271  FD_DF("SupNorm: sizeof pinv(p(L-K)): "<< rResult.Size());
272 
273  //calculate remaining set difference -> supnorm(K)
274  LanguageDifference(prK,rResult,rResult);
275  FD_DF("SupNorm: sizeof K - pinv(p(L-K)): "<< rResult.Size());
276 
277  // cosmetics: remove blocking states
278  rResult.Trim();
279  FD_DF("SupNorm: sizeof trim(K - pinv(p(L-K))): "<< rResult.Size());
280 
281  // done
282  rResult.Name("SupNorm("+rL.Name()+", "+rK.Name()+")");
283  return !( rResult.InitStatesEmpty() );
284 }
285 
286 // SupNormClosed(rL,rOAlph,rK,rResult)
288  const Generator& rL,
289  const EventSet& rOAlph,
290  const Generator& rK,
291  Generator& rResult)
292 {
293  FD_DF("SupNormClosed(" << rL.Name() << "," << rK.Name() << "," << rOAlph.Name() << ")");
294 
295  // involved operations from regular.h operate on the marked
296  // languages -> turn generated languages into marked langs
297  Generator prL=rL;
298  prL.InjectMarkedStates(prL.States());
299  Generator prK=rK;
300  prK.InjectMarkedStates(prK.States());
301 
302  // concitency check on closed languages
303  NormalityConsistencyCheck(prL,rOAlph,prK);
304 
305  //extract overall alphabet:
306  EventSet allevents;
307  allevents=rL.Alphabet();
308 
309  // calculate "L-K"
310  LanguageDifference(prL,prK,rResult);
311 
312  // calculate Pinv(P(L-K)):
313  Project(rResult,rOAlph,rResult);
314  FD_DF("SupNormClosed: sizeof p(L-K): "<< rResult.Size());
315  InvProject(rResult,allevents);
316  FD_DF("SupNormClosed: sizeof pinv(p(L-K)): "<< rResult.Size());
317 
318  //concatenate Pinv(P(L-K)) with Sigma*: this leads to closed result
319  ConcatenateFullLanguage(rResult);
320  FD_DF("SupNormClosed: sizeof pinv(p(L-K))Sigma*: "<< rResult.Size());
321 
322  //calculate remaining set difference -> supnormClosed(K)
323  LanguageDifference(prK,rResult,rResult);
324 
325  // cosmetics: remove blocking states
326  rResult.Trim();
327 
328  // done
329  rResult.Name("SupNormClosed("+rL.Name()+", "+rK.Name()+")");
330  FD_DF("SupNormClosed(" << rL.Name() << "," << rK.Name() << "," << rOAlph.Name() << "): done");
331  return !( rResult.InitStatesEmpty() );
332 }
333 
334 
335 // SupConNormClosed(rL,rCAlph,rOAlph,rK,rResult)
337  const Generator& rL,
338  const EventSet& rCAlph,
339  const EventSet& rOAlph,
340  const Generator& rK,
341  Generator& rResult)
342 {
343  FD_DF("SupConNormClosed(" << rL.Name() << "," << rK.Name() << ")");
344  // determinism required
345  ControlProblemConsistencyCheck(rL,rCAlph,rOAlph,rK);
346  // 0.: intersect K with L to match requirements of SupNormClosed
347  Generator K;
348  K.StateNamesEnabled(false);
349  Product(rL,rK,K);
350  // 1. normal and closed sublanguage (operates on / returns generated language)
351  Generator N;
352  N.StateNamesEnabled(false);
353  SupNormClosed(rL,rOAlph,K,N);
354  // 2. project to sigma_o (generated languages)
355  Generator N0,L0;
356  N0.StateNamesEnabled(false);
357  L0.StateNamesEnabled(false);
358  Project(N,rOAlph,N0);
359  Project(rL,rOAlph,L0);
360  // 3. supremal controllable sublanguage (generated languages)
361  EventSet sig_co = rCAlph * rOAlph;
362  Generator K0;
363  K0.StateNamesEnabled(false);
364  SupConClosed(L0,sig_co,N0,K0);
365  // 4. inverese project to sigma (on generated language)
366  InvProject(K0,rL.Alphabet());
367  // 5. intersect with L (generated languages)
368  LanguageIntersection(K0,rL,rResult);
369  // convenience: mark the generated language
370  rResult.InjectMarkedStates(rResult.States());
371  rResult.Name("SupConNormClosed("+rL.Name()+", "+rK.Name()+")");
372 }
373 
374 
375 // SupConNormNB(rL,rCAlph,rOAlph,rK,rResult)
377  const Generator& rL,
378  const EventSet& rCAlph,
379  const EventSet& rOAlph,
380  const Generator& rK,
381  Generator& rResult)
382 {
383  FD_DF("SupConNormNB(" << rL.Name() << "," << rK.Name() << ")");
384  // determinism required
385  ControlProblemConsistencyCheck(rL,rCAlph,rOAlph,rK);
386  // initialize: K0
387  Generator K0;
388  K0.StateNamesEnabled(false);
389  Product(rL,rK,K0);
390  K0.Coaccessible();
391  // initialize: closure(rL)
392  Generator L=rL;
393  L.StateNamesEnabled(false);
394  L.Trim();
395  L.InjectMarkedStates(L.States());
396  // loop
397  Generator Ki=K0;
398  Ki.StateNamesEnabled(false);
399  while(1) {
400  FD_DF("SupConNormNB(" << rL.Name() << "," << rK.Name() << "): #" << Ki.Size() << " m#" << Ki.MarkedStatesSize());
401  // keep copy of recent
402  rResult=Ki;
403  // cheep closure (for coreachable generator)
404  Ki.InjectMarkedStates(Ki.States());
405  // synthesise closed
406  SupConNormClosed(L,rCAlph,rOAlph,Ki,Ki);
407  // restrict
408  Product(K0,Ki,Ki);
409  Ki.Coaccessible();
410  // test (sequence is decreasing anyway)
411  if(LanguageInclusion(rResult,Ki)) break;
412  }
413  rResult.Name("SupConNormNB("+rL.Name()+", "+rK.Name()+")");
414  FD_DF("SupConNormNB(" << rL.Name() << "," << rK.Name() << "): done");
415 }
416 
417 
418 // SupPrefixClosed(rK,rResult)
420  const Generator& rK,
421  Generator& rResult)
422 {
423 
424  FD_DF("SupPrefixClosed("<<rK.Name()<<")");
425 
426  // prepare Result:
427  rResult.Name("SupPrefixClosed("+rK.Name()+")");
428 
429  // check for marked initial state, empty result if not
430  if( (rK.InitStates() * rK.MarkedStates()).Empty() ) {
431  rResult.Clear();
432  return false;
433  }
434 
435  rResult.Assign(rK);
436 
437  // erase all transitions not leading to a marked state
438  // todo: depth-first-search could be faster
439  TransSet::Iterator tit=rResult.TransRelBegin();
440  TransSet::Iterator tit_end=rResult.TransRelEnd();
441  while(tit!=tit_end) {
442  if(rResult.ExistsMarkedState(tit->X2)) { ++tit; continue;}
443  rResult.ClrTransition(tit++);
444  }
445 
446  // make reachable (cosmetic)
447  rResult.Trim();
448 
449  // as there is at least one marked init state, result is nonempty
450  return true;
451 }
452 
453 
454 // helper class
455 class SNOState {
456 public:
457  // minimal interface
458  SNOState() {};
459  SNOState(const Idx& rq, const Idx& rx, const bool& rz) :
460  q(rq), x(rx), z(rz) {};
461  std::string Str(void) { return ToStringInteger(q)+"|"+
463  // order
464  bool operator < (const SNOState& other) const {
465  if (q < other.q) return(true);
466  if (q > other.q) return(false);
467  if (x < other.x) return(true);
468  if (x > other.x) return(false);
469  if (z < other.z) return(true);
470  return(false);
471  }
472  // member variables
476 };
477 
478 
479 // SupConNormClosedUnchecked(rPlantGen, rCAlph, rOAlph, rObserverGen, rSupCandGen)
481  const Generator& rPlantGen, // aka G
482  const EventSet& rCAlph,
483  const EventSet& rOAlph,
484  Generator& rObserverGen, // aka Hobs
485  Generator& rSupCandGen // aka K
486 )
487 {
488  FD_DF("SupConNormClosedUnchecked(" << &rSupCandGen << "," << &rPlantGen << ")");
489 
490  // bail out on L(G)=0 --> closed-lopp language inclusion trivialy satisfied
491  if(rPlantGen.InitStatesEmpty()) return;
492 
493  // debugging: compare result with Lin-Brandt fromula at end of function
494  // Generator K;
495  // SupConNormClosed(rPlantGen, rCAlph, rOAlph, rSupCandGen, K);
496 
497  // loop until fixpoint
498  while(true) {
499  FD_DF("SupConNormClosedUnchecked(" << &rSupCandGen << "," << &rPlantGen << "): until fixpoint #" << rSupCandGen.Size());
500 
501  // record size to break loop
502  Idx ssz = rSupCandGen.TransRelSize();
503  Idx osz = rObserverGen.TransRelSize();
504 
505  // bail out if L(H)-0 --> closed-loop language fixpoint
506  if(rSupCandGen.InitStatesEmpty()) break;
507 
508  // todo stack (state triplets)
509  std::stack<SNOState> todo;
510  // relevant H states
511  StateSet processed, critical;
512 
513  // various iterators
514  TransSet::Iterator titg, titg_end;
515  TransSet::Iterator tith, tith_end;
516  TransSet::Iterator titho, titho_end;
517 
518  // current and successsor state
519  SNOState current, successor;
520 
521  // push combined initial state on todo stack
522  FD_DF("SupConNormClosed: todo push initial state");
523  current.q = *rPlantGen.InitStatesBegin();
524  current.x = *rSupCandGen.InitStatesBegin();
525  current.z = *rObserverGen.InitStatesBegin();
526  todo.push(current);
527 
528  // process todo stack
529  while(!todo.empty()) {
530  // allow for user interrupt, incl progress report
531  FD_WPC(1,2,"Normality(): iterating states");
532  // get top element from todo stack
533  current = todo.top();
534  todo.pop();
535  FD_DF("SupConNormClosed: todo #" << todo.size() << " processed #" << processed.Size());
536  FD_DF("SupConNormClosed: pop: (" << rPlantGen.SStr(current.q) << "|" << rSupCandGen.SStr(current.x) << ")");
537 
538  // break cycles
539  if(processed.Exists(current.x)) continue;
540  if(critical.Exists(current.x)) continue;
541 
542  // record processed
543  processed.Insert(current.x);
544 
545  // figure events disbabled by candidate K w.r.t plant G
546  EventSet disabled = rPlantGen.ActiveEventSet(current.q) - rSupCandGen.ActiveEventSet(current.x);
547 
548  // if an unobservabel event is disabled, current state becomes critical
549  if(!(disabled <= rCAlph)) {
550  critical.Insert(current.x);
551  continue;
552  }
553 
554  // disable respective transition in observer Hobs
555  titho = rObserverGen.TransRelBegin(current.z);
556  titho_end = rObserverGen.TransRelEnd(current.z);
557  while(titho!=titho_end) {
558  if(!disabled.Exists(titho->Ev)) { ++titho; continue; }
559  rObserverGen.ClrTransition(titho++);
560  }
561 
562  // find successor states to push on stack
563  titg = rPlantGen.TransRelBegin(current.q);
564  titg_end = rPlantGen.TransRelEnd(current.q);
565  tith = rSupCandGen.TransRelBegin(current.x);
566  tith_end = rSupCandGen.TransRelEnd(current.x);
567  titho = rObserverGen.TransRelBegin(current.z);
568  titho_end = rObserverGen.TransRelEnd(current.z);
569  while( (titg != titg_end) && (tith != tith_end) && (titho != titho_end) ) {
570  FD_DF("SupNorm: processing g-transition: " << rPlantGen.TStr(*titg));
571  FD_DF("SupNorm: processing h-transition: " << rSupCandGen.TStr(*tith));
572  // increment case A: process common events
573  if( (titg->Ev == tith->Ev) && (tith->Ev == titho->Ev) ) {
574  FD_DF("SupNorm: processing common event " << rPlantGen.EStr(titg->Ev));
575  // push successor
576  if(!processed.Exists(tith->X2)) {
577  successor.q=titg->X2;
578  successor.x=tith->X2;
579  successor.z=titho->X2;
580  todo.push(successor);
581  }
582  // increment
583  ++titg; ++tith; ++titho;
584  }
585  // increment case B: increment H transitions for events disabled by Hobs (when we disabled events in Hobs)
586  else if (tith->Ev < titho->Ev) {
587  rSupCandGen.ClrTransition(tith++);
588  }
589  // increment case C: increment Hobs transitions for events disabled by H (for removed critical states))
590  else if (titho->Ev < tith->Ev) {
591  ++titho;
592  }
593  // increment case D: increment G transitions for events disabled by H
594  else if (titg->Ev < tith->Ev) {
595  ++titg;
596  }
597  // increment case E: increment Hobs transitions for events disabled by G
598  else {
599  ++titho;
600  }
601  } // end accessible states
602  // reasoning for leftovers:
603  // a) if tith==end then we dont need to restrict H by Hobs anymore
604  // b) if titg=end then (by L subseteq K) we have tith=end, and we argue as in a)
605  // c) if titho=end then we need to restrict H by Hobs ...
606  while( (tith != tith_end) ) {
607  // increment case B: increment H transitions for events disabled by Hobs (when we disabled events in Hobs)
608  rSupCandGen.ClrTransition(tith++);
609  }
610 
611  } // end: todo stack
612 
613  // remove critical
614  //rSupCandGen.DelStates((rSupCandGen.States()-processed) + critical);
615  rSupCandGen.DelStates(critical);
616 
617  // break on fixpoint
618  if(ssz != rSupCandGen.TransRelSize()) continue;
619  if(osz != rObserverGen.TransRelSize()) continue;
620  break;
621 
622  } //end: until fixpoint
623 
624  // cosmetic
625  rSupCandGen.Accessible();
626 
627  /*
628  // debugging: compare with Lin-Brandt formula
629  Generator Rpr = rSupCandGen;
630  MarkAllStates(Rpr);
631  if(!LanguageEquality(K,Rpr)) FD_WARN("SUPNORM ERROR??? Supremal?");
632  */
633 
634 }
635 
636 
637 
638 /** rti wrapper */
639 void SupNorm(
640  const System& rPlantGen,
641  const Generator& rSpecGen,
642  Generator& rResGen)
643 {
644  // prepare result
645  Generator* pResGen = &rResGen;
646  if(&rResGen== &rPlantGen || &rResGen== &rSpecGen) {
647  pResGen= rResGen.New();
648  }
649  // execute
650  SupNorm(rPlantGen,rPlantGen.ObservableEvents(),rSpecGen,*pResGen);
651  // copy all attributes of input alphabet
652  pResGen->EventAttributes(rPlantGen.Alphabet());
653  // copy result
654  if(pResGen != &rResGen) {
655  pResGen->Move(rResGen);
656  delete pResGen;
657  }
658 }
659 
660 /** rti wrapper */
662  const System& rPlantGen,
663  const Generator& rSpecGen,
664  Generator& rResGen)
665 {
666  // prepare result
667  Generator* pResGen = &rResGen;
668  if(&rResGen== &rPlantGen || &rResGen== &rSpecGen) {
669  pResGen= rResGen.New();
670  }
671  // execute
672  SupNormClosed(rPlantGen,rPlantGen.ObservableEvents(),rSpecGen,*pResGen);
673  // copy all attributes of input alphabet
674  pResGen->EventAttributes(rPlantGen.Alphabet());
675  // copy result
676  if(pResGen != &rResGen) {
677  pResGen->Move(rResGen);
678  delete pResGen;
679  }
680 }
681 
682 
683 /** rti wrapper */
685  const System& rPlantGen,
686  const Generator& rSpecGen,
687  Generator& rResGen)
688 {
689  // prepare result
690  Generator* pResGen = &rResGen;
691  if(&rResGen== &rPlantGen || &rResGen== &rSpecGen) {
692  pResGen= rResGen.New();
693  }
694  // execute
695  SupConNormClosed(rPlantGen,rPlantGen.ControllableEvents(),rPlantGen.ObservableEvents(),rSpecGen,*pResGen);
696  // copy all attributes of input alphabet
697  pResGen->EventAttributes(rPlantGen.Alphabet());
698  // copy result
699  if(pResGen != &rResGen) {
700  pResGen->Move(rResGen);
701  delete pResGen;
702  }
703 }
704 
705 /** rti wrapper */
707  const System& rPlantGen,
708  const Generator& rSpecGen,
709  Generator& rResGen)
710 {
711  FD_DF("SupConNormNB(" << rPlantGen.Name() << "," << rSpecGen.Name() << "): rti wrapper");
712  // prepare result
713  Generator* pResGen = &rResGen;
714  if(&rResGen== &rPlantGen || &rResGen== &rSpecGen) {
715  pResGen= rResGen.New();
716  }
717  // execute
718  SupConNormNB(rPlantGen,rPlantGen.ControllableEvents(),rPlantGen.ObservableEvents(),rSpecGen,*pResGen);
719  // copy all attributes of input alphabet
720  pResGen->EventAttributes(rPlantGen.Alphabet());
721  // copy result
722  if(pResGen != &rResGen) {
723  pResGen->Move(rResGen);
724  delete pResGen;
725  }
726 }
727 
728 } // end namespace
#define FD_WPC(cntnow, contdone, message)
Application callback: optional write progress report to console or application, incl count
#define FD_DF(message)
Debug: optional report on user functions.
Faudes exception class.
Set of indices.
Definition: cfl_indexset.h:78
Idx Insert(void)
Insert new index to set.
Set of indices with symbolic names.
Definition: cfl_nameset.h:69
bool Exists(const Idx &rIndex) const
Test existence of index.
bool operator<(const SNOState &other) const
std::string Str(void)
SNOState(const Idx &rq, const Idx &rx, const bool &rz)
Iterator class for high-level api to TBaseSet.
Definition: cfl_baseset.h:387
Iterator BeginByX2(Idx x2) const
Iterator to first Transition specified by successor state x2.
Iterator EndByX2(Idx x2) const
Iterator to first Transition after specified successor state x2.
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Iterator on transition.
Definition: cfl_transset.h:269
const TaEventSet< EventAttr > & Alphabet(void) const
Return const reference to alphabet.
Generator with controllability attributes.
EventSet ControllableEvents(void) const
Get EventSet with controllable events.
EventSet ObservableEvents(void) const
Get EventSet with observable events.
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
Write configuration data to a string.
Definition: cfl_types.cpp:169
Base class of all FAUDES generators.
StateSet::Iterator InitStatesBegin(void) const
Iterator to Begin() of mInitStates.
const TransSet & TransRel(void) const
Return reference to transition relation.
bool SetTransition(Idx x1, Idx ev, Idx x2)
Add a transition to generator by indices.
const StateSet & MarkedStates(void) const
Return const ref of marked states.
const EventSet & Alphabet(void) const
Return const reference to alphabet.
void ClearTransRel(void)
Clear all transitions.
virtual void Move(vGenerator &rGen)
Destructive copy to other vGenerator.
virtual vGenerator & Assign(const Type &rSrc)
Copy from other faudes type.
bool InitStatesEmpty(void) const
Check if set of initial states are empty.
EventSet ActiveEventSet(Idx x1) const
Return active event set at state x1.
const StateSet & InitStates(void) const
Const ref to initial states.
TransSet::Iterator TransRelBegin(void) const
Iterator to Begin() of transition relation.
void ClrTransition(Idx x1, Idx ev, Idx x2)
Remove a transition by indices.
bool Accessible(void)
Make generator accessible.
bool Trim(void)
Make generator trim.
void ClearStates(void)
Clear all states and transitions, maintain alphabet.
EventSet::Iterator AlphabetBegin(void) const
Iterator to Begin() of alphabet.
virtual vGenerator * New(void) const
Construct on heap.
void InjectMarkedStates(const StateSet &rNewMarkedStates)
Replace mMarkedStates with StateSet given as parameter without consistency checks.
Idx MarkedStatesSize(void) const
Get number of marked states.
StateSet::Iterator MarkedStatesBegin(void) const
Iterator to Begin() of mMarkedStates.
bool Coaccessible(void)
Make generator Coaccessible.
std::string TStr(const Transition &rTrans) const
Return pretty printable transition (eg for debugging)
void Name(const std::string &rName)
Set the generator's name.
void DelStates(const StateSet &rDelStates)
Delete a set of states Cleans mpStates, mInitStates, mMarkedStates, mpTransrel, and mpStateSymboltabl...
TransSet::Iterator TransRelEnd(void) const
Iterator to End() of transition relation.
bool IsDeterministic(void) const
Check if generator is deterministic.
std::string EStr(Idx index) const
Pretty printable event name for index (eg for debugging).
StateSet::Iterator MarkedStatesEnd(void) const
Iterator to End() of mMarkedStates.
void SetMarkedState(Idx index)
Set an existing state as marked state by index.
Idx InsInitState(void)
Create new anonymous state and set as initial state.
virtual void EventAttributes(const EventSet &rEventSet)
Set attributes for existing events.
bool StateNamesEnabled(void) const
Whether libFAUEDS functions are requested to generate state names.
Idx TransRelSize(void) const
Get number of transitions.
EventSet::Iterator AlphabetEnd(void) const
Iterator to End() of alphabet.
Idx Size(void) const
Get generator size (number of states)
std::string SStr(Idx index) const
Return pretty printable state name for index (eg for debugging)
virtual void Clear(void)
Clear generator data.
bool ExistsMarkedState(Idx index) const
Test existence of state in mMarkedStates.
const StateSet & States(void) const
Return reference to state set.
bool Empty(void) const
Test whether if the TBaseSet is Empty.
Definition: cfl_baseset.h:1824
bool Exists(const T &rElem) const
Test existence of element.
Definition: cfl_baseset.h:2115
const std::string & Name(void) const
Return name of TBaseSet.
Definition: cfl_baseset.h:1755
Idx Size(void) const
Get Size of TBaseSet.
Definition: cfl_baseset.h:1819
bool LanguageInclusion(const Generator &rGen1, const Generator &rGen2)
Test language inclusion, Lm1<=Lm2.
void Product(const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
Product composition.
bool IsEmptyLanguage(const Generator &rGen)
Test for Empty language Lm(G)=={}.
void LanguageDifference(const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
Language difference (set-theoretic difference).
void LanguageIntersection(const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
Language intersection.
void Project(const Generator &rGen, const EventSet &rProjectAlphabet, Generator &rResGen)
Deterministic projection.
void InvProject(Generator &rGen, const EventSet &rProjectAlphabet)
Inverse projection.
bool SupNorm(const Generator &rL, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
SupNorm: compute supremal normal sublanguage.
bool IsNormal(const Generator &rL, const EventSet &rOAlph, const Generator &rK)
IsNormal: checks normality of a language K generated by rK wrt a language L generated by rL and the s...
void SupConNormClosed(const Generator &rL, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
SupConNormClosed: compute supremal controllable, normal and closed sublanguage.
void SupConNormNB(const Generator &rL, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
SupConNormNB: compute supremal controllable and normal sublanguage.
void SupConClosed(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
Supremal Controllable and Closed Sublanguage.
Definition: syn_supcon.cpp:778
bool SupNormClosed(const Generator &rL, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
SupNormClosed - compute supremal normal and closed sublanguage.
libFAUDES resides within the namespace faudes.
uint32_t Idx
Type definition for index type (allways 32bit)
void NormalityConsistencyCheck(const Generator &rL, const EventSet &rOAlph, const Generator &rK)
NormalityConsistencyCheck: Consistency check for normality input data.
Definition: syn_supnorm.cpp:45
void SupConNormClosedUnchecked(const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rOAlph, Generator &rObserverGen, Generator &rSupCandGen)
Supremal Normal Controllable Sublangauge (internal function)
bool SupPrefixClosed(const Generator &rK, Generator &rResult)
SupPrefixClosed: supremal closed sublanguage of K by cancelling all tranistions leading to a non-mark...
void ConcatenateFullLanguage(Generator &rGen)
ConcatenateFullLanguage: concatenate Sigma* to language marked by rGen.
void ControlProblemConsistencyCheck(const GeneratorVector &rPlantGenVec, const EventSet &rConAlph, const GeneratorVector &rSpecGenVec)
Compositional synthesis.
std::string ToStringInteger(Int number)
integer to string
Definition: cfl_helper.cpp:43
Supremal controllable sublanguage.
Supremal normal sublanguage.

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