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)
#define FD_DF(message)
bool Exists(const Idx &rIndex) const
bool operator<(const SNOState &other) const
std::string Str(void)
SNOState(const Idx &rq, const Idx &rx, const bool &rz)
Iterator BeginByX2(Idx x2) const
Iterator EndByX2(Idx x2) const
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Definition: cfl_transset.h:273
const TaEventSet< EventAttr > & Alphabet(void) const
EventSet ControllableEvents(void) const
EventSet ObservableEvents(void) const
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
Definition: cfl_types.cpp:170
StateSet::Iterator InitStatesBegin(void) const
const TransSet & TransRel(void) const
bool SetTransition(Idx x1, Idx ev, Idx x2)
const StateSet & MarkedStates(void) const
const EventSet & Alphabet(void) const
virtual void Move(vGenerator &rGen)
virtual vGenerator & Assign(const Type &rSrc)
bool InitStatesEmpty(void) const
EventSet ActiveEventSet(Idx x1) const
const StateSet & InitStates(void) const
TransSet::Iterator TransRelBegin(void) const
void ClrTransition(Idx x1, Idx ev, Idx x2)
EventSet::Iterator AlphabetBegin(void) const
virtual vGenerator * New(void) const
void InjectMarkedStates(const StateSet &rNewMarkedStates)
Idx MarkedStatesSize(void) const
StateSet::Iterator MarkedStatesBegin(void) const
std::string TStr(const Transition &rTrans) const
void Name(const std::string &rName)
void DelStates(const StateSet &rDelStates)
TransSet::Iterator TransRelEnd(void) const
bool IsDeterministic(void) const
std::string EStr(Idx index) const
StateSet::Iterator MarkedStatesEnd(void) const
void SetMarkedState(Idx index)
virtual void EventAttributes(const EventSet &rEventSet)
bool StateNamesEnabled(void) const
Idx TransRelSize(void) const
EventSet::Iterator AlphabetEnd(void) const
Idx Size(void) const
std::string SStr(Idx index) const
virtual void Clear(void)
bool ExistsMarkedState(Idx index) const
const StateSet & States(void) const
bool Empty(void) const
Definition: cfl_baseset.h:1841
bool Exists(const T &rElem) const
Definition: cfl_baseset.h:2132
const std::string & Name(void) const
Definition: cfl_baseset.h:1772
Idx Size(void) const
Definition: cfl_baseset.h:1836
bool LanguageInclusion(const Generator &rGen1, const Generator &rGen2)
void Product(const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
bool IsEmptyLanguage(const Generator &rGen)
void LanguageDifference(const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
void LanguageIntersection(const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
void Project(const Generator &rGen, const EventSet &rProjectAlphabet, Generator &rResGen)
void InvProject(Generator &rGen, const EventSet &rProjectAlphabet)
bool SupNorm(const Generator &rL, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
bool IsNormal(const Generator &rL, const EventSet &rOAlph, const Generator &rK)
void SupConNormClosed(const Generator &rL, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
void SupConNormNB(const Generator &rL, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
void SupConClosed(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
Definition: syn_supcon.cpp:778
bool SupNormClosed(const Generator &rL, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
uint32_t Idx
void NormalityConsistencyCheck(const Generator &rL, const EventSet &rOAlph, const Generator &rK)
Definition: syn_supnorm.cpp:45
void SupConNormClosedUnchecked(const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rOAlph, Generator &rObserverGen, Generator &rSupCandGen)
bool SupPrefixClosed(const Generator &rK, Generator &rResult)
void ConcatenateFullLanguage(Generator &rGen)
void ControlProblemConsistencyCheck(const GeneratorVector &rPlantGenVec, const EventSet &rConAlph, const GeneratorVector &rSpecGenVec)
std::string ToStringInteger(Int number)
Definition: cfl_utils.cpp:43

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