mtc_supcon.cpp
Go to the documentation of this file.
1 /** @file mtc_supcon.cpp
2 
3 Supremal controllable sublanguage and controllablity
4 
5 */
6 
7 /* FAU Discrete Event Systems Library (libfaudes)
8 
9  Copyright (C) 2008 Matthias Singer
10  Copyright (C) 2006 Bernd Opitz
11  Exclusive copyright is granted to Klaus Schmidt
12 
13  This library is free software; you can redistribute it and/or
14  modify it under the terms of the GNU Lesser General Public
15  License as published by the Free Software Foundation; either
16  version 2.1 of the License, or (at your option) any later version.
17 
18  This library is distributed in the hope that it will be useful,
19  but WITHOUT ANY WARRANTY; without even the implied warranty of
20  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
21  Lesser General Public License for more details.
22 
23  You should have received a copy of the GNU Lesser General Public
24  License along with this library; if not, write to the Free Software
25  Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA */
26 
27 
28 #include "mtc_supcon.h"
29 #include "syn_include.h"
30 
31 namespace faudes {
32 
33 /*
34 ******************************
35 * SUPCON: USER FUNCTIONS *
36 ******************************
37 */
38 
39 
40 // mtcSupCon(rPlantGen, rSpecGen, rResGen)
41 void mtcSupCon(const MtcSystem& rPlantGen, const MtcSystem& rSpecGen, MtcSystem& rResGen) {
42  // HELPERS:
43  std::map< std::pair<Idx,Idx>, Idx> rcmap;
44  // ALGORITHM:
45  mtcSupCon(rPlantGen, rSpecGen, rcmap, rResGen);
46 }
47 
48 
49 // mtcSupCon(rPlantGen, rSpecGen, rReverseCompositionMap, rResGen)
50 void mtcSupCon(const MtcSystem& rPlantGen, const MtcSystem& rSpecGen,
51  std::map< std::pair<Idx,Idx>, Idx>& rCompositionMap, MtcSystem& rResGen) {
52  FD_DF("mtcSupCon(" << &rPlantGen << "," << &rSpecGen << ")");
53 
54  // PREPARE RESULT:
55 
56  rResGen.Clear();
57  rResGen.Name("mtcSupCon(("+rPlantGen.Name()+"),("+rSpecGen.Name()+"))");
58  rResGen.InjectAlphabet(rPlantGen.Alphabet());
59 
60  rResGen.SetControllable(rPlantGen.ControllableEvents());
61  rResGen.SetForcible(rPlantGen.ForcibleEvents());
62  rResGen.ClrObservable(rPlantGen.UnobservableEvents());
63 
64  // HELPERS:
65 
66  // controllable events
67  const EventSet ualph = rPlantGen.UncontrollableEvents();
68  FD_DF("mtcSupCon: controllable events: " << rPlantGen.ControllableEvents().ToString());
69  FD_DF("mtcSupCon: uncontrollable events: " << ualph.ToString());
70 
71  // CONSISTENCY CHECK:
72 
73  // alphabets must match
74  if (rPlantGen.Alphabet() != rSpecGen.Alphabet()) {
75  EventSet only_in_plant = rPlantGen.Alphabet() - rSpecGen.Alphabet();
76  EventSet only_in_spec = rSpecGen.Alphabet() - rPlantGen.Alphabet();
77  std::stringstream errstr;
78  errstr << "Alphabets of generators do not match. Only in plant: " << only_in_plant.ToString()
79  << ". Only in spec: " << only_in_spec.ToString() << ".";
80  throw Exception("mtcSupCon", errstr.str(), 500);
81  }
82 
83  // plant and spec must be deterministic
84  bool plant_det = rPlantGen.IsDeterministic();
85  bool spec_det = rSpecGen.IsDeterministic();
86 
87  if ((plant_det == false) && (spec_det == true)) {
88  std::stringstream errstr;
89  errstr << "Plant generator must be deterministic, "
90  << "but is nondeterministic";
91  throw Exception("mtcSupCon", errstr.str(), 501);
92  }
93  else if ((plant_det == true) && (spec_det == false)) {
94  std::stringstream errstr;
95  errstr << "Spec generator must be deterministic, "
96  << "but is nondeterministic";
97  throw Exception("mtcSupCon", errstr.str(), 503);
98  }
99  else if ((plant_det == false) && (spec_det == false)) {
100  std::stringstream errstr;
101  errstr << "Plant and spec generator must be deterministic, "
102  << "but both are nondeterministic";
103  throw Exception("mtcSupCon", errstr.str(), 504);
104  }
105 
106  // ALGORITHM:
107 
108  mtcSupConParallel(rPlantGen, rSpecGen, ualph, rCompositionMap, rResGen);
109  FD_DF("mtcSupCon: mtcSupConParallel passed...");
110 
111  // make resulting generator trim until it's fully controllable
112  while (1) {
113  if(rResGen.Empty()) break;
114  Idx state_num = rResGen.Size();
115  mtcSupConUnchecked(rPlantGen, rPlantGen.ControllableEvents(), rResGen);
116  rResGen.StronglyTrim();
117  if(rResGen.Size() == state_num) break;
118  FD_DF("mtcSupCon: rResGen.Size() = " << ToStringInteger(rResGen.Size()) << ", state_num = " << ToStringInteger(state_num));
119  }
120 
121  // restrict composition map
122  std::map< std::pair<Idx,Idx>, Idx>::iterator rcmapit = rCompositionMap.begin();
123  for(; rcmapit != rCompositionMap.end(); rcmapit++)
124  if(!rResGen.ExistsState(rcmapit->second)) rCompositionMap.erase(rcmapit++);
125 
126 
127 }
128 
129 // mtcSupConClosed(rPlantGen, rSpecGen, rResGen)
130 void mtcSupConClosed(const MtcSystem& rPlantGen, const MtcSystem& rSpecGen, MtcSystem& rResGen) {
131  // HELPERS:
132  std::map< std::pair<Idx,Idx>, Idx> rcmap;
133 
134  // ALGORITHM:
135  mtcSupConClosed(rPlantGen, rSpecGen, rcmap, rResGen);
136 }
137 
138 
139 // mtcSupConClosed(rPlantGen, rSpecGen, rCompositionMap, rResGen)
140 void mtcSupConClosed(const MtcSystem& rPlantGen, const MtcSystem& rSpecGen,
141  std::map< std::pair<Idx,Idx>, Idx>& rCompositionMap, MtcSystem& rResGen) {
142  FD_DF("mtcSupConClosed(" << &rPlantGen << "," << &rSpecGen << ")");
143 
144  // PREPARE RESULT:
145  rResGen.Clear();
146  rResGen.Name("mtcSupConClosed(("+rPlantGen.Name()+"),("+rSpecGen.Name()+"))");
147 
148  rResGen.InjectAlphabet(rPlantGen.Alphabet());
149 
150  rResGen.SetControllable(rPlantGen.ControllableEvents());
151  rResGen.SetForcible(rPlantGen.ForcibleEvents());
152  rResGen.ClrObservable(rPlantGen.UnobservableEvents());
153 
154  // HELPERS:
155 
156  // controllable events
157  const EventSet ualph = rPlantGen.UncontrollableEvents();
158  FD_DF("mtcSupConClosed: controllable events: " << rPlantGen.ControllableEvents().ToString());
159  FD_DF("mtcSupConClosed: uncontrollable events: " << ualph.ToString());
160 
161  // CONSISTENCY CHECK:
162 
163  // alphabets must match
164  if (rPlantGen.Alphabet() != rSpecGen.Alphabet()) {
165  EventSet only_in_plant = rPlantGen.Alphabet() - rSpecGen.Alphabet();
166  EventSet only_in_spec = rSpecGen.Alphabet() - rPlantGen.Alphabet();
167  std::stringstream errstr;
168  errstr << "Alphabets of generators do not match. Only in plant: "
169  << only_in_plant.ToString() << ". Only in spec: "
170  << only_in_spec.ToString() << ".";
171  throw Exception("mtcSupConClosed", errstr.str(), 500);
172  }
173 
174  // plant and spec must be deterministic
175  bool plant_det = rPlantGen.IsDeterministic();
176  bool spec_det = rSpecGen.IsDeterministic();
177 
178  if ((plant_det == false) && (spec_det == true)) {
179  std::stringstream errstr;
180  errstr << "Plant generator must be deterministic, " << "but is nondeterministic";
181  throw Exception("mtcSupConClosed", errstr.str(), 501);
182  }
183  else if ((plant_det == true) && (spec_det == false)) {
184  std::stringstream errstr;
185  errstr << "Spec generator must be deterministic, " << "but is nondeterministic";
186  throw Exception("mtcSupConClosed", errstr.str(), 503);
187  }
188  else if ((plant_det == false) && (spec_det == false)) {
189  std::stringstream errstr;
190  errstr << "Plant and spec generator must be deterministic, "
191  << "but both are nondeterministic";
192  throw Exception("mtcSupCon", errstr.str(), 504);
193  }
194 
195  // ALGORITHM:
196 
197  // parallel composition
198  mtcSupConParallel(rPlantGen, rSpecGen, ualph, rCompositionMap, rResGen);
199  // make resulting generator controllable
200  mtcSupConUnchecked(rPlantGen, rPlantGen.ControllableEvents(), rResGen);
201 
202  // restrict composition map
203  std::map< std::pair<Idx,Idx>, Idx>::iterator rcmapit = rCompositionMap.begin();
204  for(; rcmapit != rCompositionMap.end(); rcmapit++)
205  if(!rResGen.ExistsState(rcmapit->second)) rCompositionMap.erase(rcmapit++);
206 
207 
208 }
209 
210 
211 
212 /*
213 ********************************************
214 * Fast parallel composition for mtcSupCon *
215 ********************************************
216 */
217 
218 
219 // mtcSupConParallel(rPlantGen, rSpecGen, rUAlph, rReverseCompositionMap, rResGen)
220 void mtcSupConParallel(const MtcSystem& rPlantGen, const MtcSystem& rSpecGen, const EventSet& rUAlph,
221  std::map< std::pair<Idx,Idx>, Idx>& rReverseCompositionMap, MtcSystem& rResGen) {
222  FD_DF("mtcSupConParallel(" << &rPlantGen << "," << &rSpecGen << ")");
223 
224  // HELPERS:
225 
226  // todo stack
227  std::stack< std::pair<Idx,Idx> > todo;
228  // set of forbidden states
229  StateSet forbidden;
230  // actual pair, new pair
231  std::pair<Idx,Idx> currentstates, newstates;
232  // other stuff
233  Idx tmpstate;
234  std::map< std::pair<Idx,Idx>, Idx>::iterator rcmapit;
235  StateSet::Iterator lit1, lit2;
236  TransSet::Iterator titg, titg_end, tith, tith_end;
237 
238  // Prepare
239  rResGen.ClearStates();
240 
241  // ALGORITHM:
242  if (rPlantGen.InitStatesEmpty()) {
243  FD_DF("SupconParallel: plant got no initial states. "
244  << "parallel composition contains empty language.");
245  return;
246  }
247 
248  if (rSpecGen.InitStatesEmpty()) {
249  FD_DF("mtcSupConParallel: spec got no initial states. "
250  << "parallel composition contains empty language.");
251  return;
252  }
253  ColorSet plantColors = rPlantGen.Colors();
254  ColorSet specColors = rSpecGen.Colors();
255  // create initial state
256  currentstates = std::make_pair(*rPlantGen.InitStatesBegin(), *rSpecGen.InitStatesBegin());
257  todo.push(currentstates);
258  ColorSet ComposedSet;
259  ComposedColorSet(rPlantGen, currentstates.first, plantColors, rSpecGen, currentstates.second,
260  specColors, ComposedSet);
261  if (! ComposedSet.Empty() ) {
262  Idx StateIndex = rResGen.InsInitState();
263  rReverseCompositionMap[currentstates] = StateIndex;
264  rResGen.InsColors(StateIndex, ComposedSet);
265  FD_DF("mtcSupConParallel: NEW IMSTATE: (" << rPlantGen.SStr(currentstates.first)
266  << "|" << rSpecGen.SStr(currentstates.second) << ") -> " << rReverseCompositionMap[currentstates]);
267  }
268  else {
269  rReverseCompositionMap[currentstates] = rResGen.InsInitState();
270  FD_DF("mtcSupConParallel: NEW ISTATE: (" << rPlantGen.SStr(currentstates.first)
271  << "|" << rSpecGen.SStr(currentstates.second) << ") -> " << rReverseCompositionMap[currentstates]);
272  }
273 
274  // first do parallel composition of allowed states
275  // by deleting forbidden states on the fly.
276  // this creates an accessible new generator
277  FD_DF("mtcSupConParallel: *** processing reachable states ***");
278  while (! todo.empty()) {
279  // get next reachable pair of states from todo stack
280  currentstates = todo.top();
281  todo.pop();
282  FD_DF("mtcSupConParallel: todo pop: (" << rPlantGen.SStr(currentstates.first)
283  << "|" << rSpecGen.SStr(currentstates.second) << ") -> " << rReverseCompositionMap[currentstates]);
284 
285  titg = rPlantGen.TransRelBegin(currentstates.first);
286  titg_end = rPlantGen.TransRelEnd(currentstates.first);
287  tith = rSpecGen.TransRelBegin(currentstates.second);
288  tith_end = rSpecGen.TransRelEnd(currentstates.second);
289 
290 #ifdef FAUDES_DEBUG_FUNCTION
291  // print all transitions of current states
292  FD_DF("mtcSupConParallel: transitions from current states:");
293  for (;titg != titg_end; ++titg) {
294  FD_DF("mtcSupConParallel: g: " << rPlantGen.SStr(titg->X1) << "-" << rPlantGen.EStr(titg->Ev)
295  << "-" << rPlantGen.SStr(titg->X2));
296  }
297  for (;tith != tith_end; ++tith) {
298  FD_DF("mtcSupConParallel: h: " << rSpecGen.SStr(tith->X1) << "-" << rSpecGen.EStr(tith->Ev)
299  << "-" << rSpecGen.SStr(tith->X2));
300  }
301  titg = rPlantGen.TransRelBegin(currentstates.first);
302  tith = rSpecGen.TransRelBegin(currentstates.second);
303 #endif
304  // process all h transitions while there could be matching g transitions
305  while ((tith != tith_end) && (titg != titg_end)) {
306  FD_DF("mtcSupConParallel: actual g-transition: " << rPlantGen.SStr(titg->X1)
307  << "-" << rPlantGen.EStr(titg->Ev) << "-" << rPlantGen.SStr(titg->X2));
308  FD_DF("mtcSupConParallel: actual h-transition: " << rSpecGen.SStr(tith->X1)
309  << "-" << rSpecGen.EStr(tith->Ev) << "-" << rSpecGen.SStr(tith->X2));
310  // execute common events
311  if (titg->Ev == tith->Ev) {
312  FD_DF("mtcSupConParallel: executing common event "
313  << rPlantGen.EStr(titg->Ev));
314  newstates = std::make_pair(titg->X2, tith->X2);
315  rcmapit = rReverseCompositionMap.find(newstates);
316  // add to todo list if state is new
317  if (rcmapit == rReverseCompositionMap.end()) {
318  todo.push(newstates);
319  // if colored state
320  ComposedColorSet(rPlantGen, newstates.first, plantColors, rSpecGen, newstates.second,
321  specColors, ComposedSet);
322  if(!ComposedSet.Empty() ) {
323  tmpstate = rResGen.InsState();
324  rResGen.InsColors(tmpstate, ComposedSet);
325  FD_DF("mtcSupConParallel: NEW MSTATE: ("
326  << rPlantGen.SStr(newstates.first) << "|"
327  << rSpecGen.SStr(newstates.second) << ") -> " << tmpstate);
328  }
329  // if "normal" state
330  else {
331  tmpstate = rResGen.InsState();
332  FD_DF("mtcSupConParallel: NEW STATE: ("
333  << rPlantGen.SStr(newstates.first) << "|"
334  << rSpecGen.SStr(newstates.second) << ") -> " << tmpstate);
335  }
336  rReverseCompositionMap[newstates] = tmpstate;
337  FD_DF("mtcSupConParallel: todo push: (" << rPlantGen.SStr(newstates.first)
338  << "|" << rSpecGen.SStr(newstates.second) << ") -> " << tmpstate);
339  }
340  // if state already exists
341  else {
342  tmpstate = rcmapit->second;
343  }
344  // if successor state not in forbidden set add transition
345  if (! forbidden.Exists(tmpstate)) {
346  FD_DF("mtcSupConParallel: ADDING TRANSITION "
347  << rPlantGen.SStr(rReverseCompositionMap[currentstates]) << "-" << rPlantGen.EStr(titg->Ev)
348  << "-" << rPlantGen.SStr(tmpstate));
349  rResGen.SetTransition(rReverseCompositionMap[currentstates], titg->Ev, tmpstate);
350  FD_DF("mtcSupConParallel: incrementing g transrel");
351  ++titg;
352  FD_DF("mtcSupConParallel: incrementing h transrel");
353  ++tith;
354  }
355  // if successor state in forbidden and event uncontrollable
356  // delete state
357  else if (rUAlph.Exists(titg->Ev)) {
358  FD_DF("mtcSupConParallel: successor " << rSpecGen.SStr(tmpstate)
359  << "in forbidden and common event " << rSpecGen.EStr(titg->Ev)
360  << " uncontrollable:");
361  FD_DF("mtcSupConParallel: forbidden insert" << rPlantGen.SStr(tmpstate));
362  forbidden.Insert(tmpstate);
363 #ifdef FAUDES_CHECKED
364  // do not end while loops here for detecting all h transitions
365  // not in g
366  FD_DF("mtcSupConParallel: incrementing g transrel (FAUDES_CHECKED)");
367  ++titg;
368  FD_DF("mtcSupConParallel: incrementing h transrel (FAUDES_CHECKED)");
369  ++tith;
370 #else
371  // exit all loops
372  titg = titg_end;
373  tith = tith_end;
374 #endif
375  }
376  // else if successor state in forbidden and event controllable
377  else {
378  FD_DF("mtcSupConParallel: incrementing g transrel");
379  ++titg;
380  FD_DF("mtcSupConParallel: incrementing h transrel");
381  ++tith;
382  }
383  }
384  // if g got some more transitions try to resync events
385  else if (titg->Ev < tith->Ev) {
386  FD_DF("mtcSupConParallel: asynchronous execution of event "
387  << rPlantGen.EStr(titg->Ev) << " in g while " << rSpecGen.EStr(tith->Ev)
388  << " in h");
389  // if uncontrollable transition leaves specification
390  // delete state from res and put into forbiddenset
391  if (rUAlph.Exists(titg->Ev)) {
392  FD_DF("mtcSupConParallel: asynchronous event " << rPlantGen.EStr(titg->Ev)
393  << " in g is uncontrollable");
394  tmpstate = rReverseCompositionMap[currentstates];
395  FD_DF("mtcSupConParallel: forbidden insert" << rPlantGen.SStr(tmpstate));
396  forbidden.Insert(tmpstate);
397  // exit all loops
398  titg = titg_end;
399  tith = tith_end;
400  break;
401  }
402  FD_DF("mtcSupConParallel: incrementing g transrel");
403  ++titg;
404  } // if specification leaves plant model emit warning
405  else {
406 #ifdef FAUDES_CHECKED
407 // FD_WARN("mtcSupConParallel: transition " << rSpecGen.SStr(tith->X1)
408 // << "-" << rSpecGen.EStr(tith->Ev) << "-" << rSpecGen.SStr(tith->X2)
409 // << " in specification h not found in g");
410 #endif
411  FD_DF("mtcSupConParallel: incrementing h transrel");
412  ++tith;
413  }
414  }
415  if (rResGen.InitStates().Empty()) {
416  FD_DF("mtcSupConParallel: rResGen has no initial states... (2)");
417  }
418 
419  // if g got some more transitions not in h
420  while (titg != titg_end) {
421  FD_DF("mtcSupConParallel: asynchronous execution of event "
422  << rPlantGen.EStr(titg->Ev) << " in g at end of h");
423  FD_DF("mtcSupConParallel: actual g-transition: " << rPlantGen.SStr(titg->X1)
424  << "-" << rPlantGen.EStr(titg->Ev) << "-" << rPlantGen.SStr(titg->X2));
425  FD_DF("mtcSupConParallel: actual h-transition: end");
426  // if uncontrollable transition leaves specification
427  if (rUAlph.Exists(titg->Ev)) {
428  tmpstate = rReverseCompositionMap[currentstates];
429  FD_DF("mtcSupConParallel: asynchron executed uncontrollable end "
430  << "event " << rPlantGen.EStr(titg->Ev) << " leaves specification:");
431  FD_DF("mtcSupConParallel: forbidden insert" << rPlantGen.SStr(tmpstate));
432  forbidden.Insert(tmpstate);
433  // exit this loop
434  // if FAUDES_CHECKED not defined this means exiting all loops
435  break;
436  }
437  FD_DF("mtcSupConParallel: incrementing g transrel");
438  ++titg;
439  }
440 #ifdef FAUDES_CHECKED
441  // if h got some more transitions not in g
442 // while (tith != tith_end) {
443 // FD_WARN("mtcSupConParallel: transition " << rSpecGen.SStr(tith->X1) << "-"
444 // << rSpecGen.EStr(tith->Ev) << "-" << rSpecGen.SStr(tith->X2)
445 // << "in specification h not found in g");
446 // FD_DF("mtcSupConParallel: incrementing h transrel");
447 // ++tith;
448 // }
449 #endif
450  }
451  FD_DF("mtcSupConParallel: deleting forbidden states...");
452  // remove forbidden states from stateset
453  rResGen.DelStates(forbidden);
454 }
455 
456 /*
457 *****************************************
458 * mtcSupConUnchecked: REAL SUPCON FUNCTION *
459 *****************************************
460 */
461 
462 
463 // mtcSupConUnchecked(rPlantGen, rSpecGen, rCAlph)
464 void mtcSupConUnchecked(const MtcSystem& rPlantGen, const EventSet& rCAlph, MtcSystem& rSpecGen) {
465 
466  FD_DF("mtcSupConUnchecked(" << &rSpecGen << "," << &rPlantGen << ")");
467 
468  // HELPERS:
469 
470  // forbiden states
471  StateSet forbidden;
472  // todo stack
473  std::stack<Idx> todog, todoh;
474  // set of already discovered states
475  StateSet discovered;
476  // reverse sorted transition relation build on the fly
477  TransSetX2EvX1 rtransrel;
478 
479 
480  // ALGORITHM:
481 
482  // bail out if there is no initial state
483  // if (rPlantGen.InitStatesEmpty() || rSpecGen.InitStatesEmpty());
484 
485  // push combined initial state on todo stack
486  todog.push(*rPlantGen.InitStatesBegin());
487  todoh.push(*rSpecGen.InitStatesBegin());
488  FD_DF("mtcSupCon: todo push: (" << rPlantGen.SStr(*rPlantGen.InitStatesBegin()) << "|"
489  << rSpecGen.SStr(*rSpecGen.InitStatesBegin()) << ")");
490 
491  // process todo stack
492  while (! todog.empty()) {
493  // get top elements from todo stack
494  Idx currentg = todog.top();
495  Idx currenth = todoh.top();
496  todog.pop();
497  todoh.pop();
498  FD_DF("mtcSupCon: todo pop: (" << rPlantGen.SStr(currentg) << "|"
499  << rSpecGen.SStr(currenth) << ")");
500 
501 #ifdef FAUDES_DEBUG_FUNCTION
502  TransSet::Iterator _titg, _tith;
503  // print all transitions of current states
504  FD_DF("mtcSupCon: transitions from current states:");
505  for (_titg = rPlantGen.TransRelBegin(currentg); _titg != rPlantGen.TransRelEnd(currentg); ++_titg)
506  FD_DF("mtcSupCon: g: " << rPlantGen.SStr(_titg->X1) << "-"
507  << rPlantGen.EStr(_titg->Ev) << "-" << rPlantGen.SStr(_titg->X2));
508  for (_tith = rSpecGen.TransRelBegin(currenth); _tith != rSpecGen.TransRelEnd(currenth); ++_tith)
509  FD_DF("mtcSupCon: h: " << rSpecGen.SStr(_tith->X1) << "-"
510  << rSpecGen.EStr(_tith->Ev) << "-" << rSpecGen.SStr(_tith->X2));
511 #endif
512 
513  // process all h transitions while there could be matching g transitions
514  TransSet::Iterator titg = rPlantGen.TransRelBegin(currentg);
515  TransSet::Iterator titg_end = rPlantGen.TransRelEnd(currentg);
516  TransSet::Iterator tith = rSpecGen.TransRelBegin(currenth);
517  TransSet::Iterator tith_end = rSpecGen.TransRelEnd(currenth);
518  while ((tith != tith_end) && (titg != titg_end)) {
519  FD_DF("mtcSupCon: actual g-transition: " << rPlantGen.SStr(titg->X1)
520  << "-" << rPlantGen.EStr(titg->Ev) << "-" << rPlantGen.SStr(titg->X2));
521  FD_DF("mtcSupCon: actual h-transition: " << rSpecGen.SStr(tith->X1)
522  << "-" << rSpecGen.EStr(tith->Ev) << "-" << rSpecGen.SStr(tith->X2));
523  // execute common events
524  if (titg->Ev == tith->Ev) {
525  FD_DF("mtcSupCon: executing common event " << rPlantGen.EStr(titg->Ev));
526  // add to todo list if state is undiscovered
527  if (! discovered.Exists(currenth)) {
528  todog.push(titg->X2);
529  todoh.push(tith->X2);
530  FD_DF("mtcSupCon: todo push: (" << rPlantGen.SStr(titg->X2) << "|"
531  << rSpecGen.SStr(tith->X2) << ")");
532  }
533  // if h successor state not in forbidden set add transition to rtransrel
534  if (! forbidden.Exists(tith->X2)) {
535  rtransrel.Insert(*tith);
536  FD_DF("mtcSupCon: incrementing g transrel");
537  ++titg;
538  FD_DF("mtcSupCon: incrementing h transrel");
539  ++tith;
540  }
541  // if successor state is forbidden and event uncontrollable
542  else if (!rCAlph.Exists(titg->Ev)) {
543  FD_DF("mtcSupCon: successor state " << rSpecGen.SStr(tith->X2) <<
544  " forbidden and event " << rPlantGen.EStr(titg->Ev) << " uncontrollable:");
545  FD_DF("mtcSupCon: TraverseUncontrollableBackwards(" << rSpecGen.SStr(currenth) << ")");
546  TraverseUncontrollableBackwards(rCAlph, rtransrel, forbidden, currenth);
547 #ifdef FAUDES_CHECKED
548  // just increment transrel iterators to find all h transitions not in g
549  FD_DF("mtcSupCon: incrementing g transrel (FAUDES_CHECKED)");
550  ++titg;
551  FD_DF("mtcSupCon: incrementing h transrel (FAUDES_CHECKED)");
552  ++tith;
553 #else
554  // exit all loops
555  titg = titg_end;
556  tith = tith_end;
557 #endif
558  break;
559  }
560  // else if successor state in forbidden and event controllable
561  else {
562  FD_DF("mtcSupCon: incrementing g transrel");
563  ++titg;
564  FD_DF("mtcSupCon: incrementing h transrel");
565  ++tith;
566  }
567  }
568  // if g got some more transitions try to resync events
569  else if (titg->Ev < tith->Ev) {
570  FD_DF("mtcSupCon: asynchronous execution of event "
571  << rPlantGen.EStr(titg->Ev) << " in g while " << rSpecGen.EStr(tith->Ev)
572  << " in h");
573  // if uncontrollable transition leaves specification
574  // delete state from rResGen and put into forbiddenset
575  if (!rCAlph.Exists(titg->Ev)) {
576  FD_DF("mtcSupCon: asynchronous event " << rPlantGen.EStr(titg->Ev)
577  << " in g is uncontrollable");
578  FD_DF("mtcSupCon: TraverseUncontrollableBackwards(" << rSpecGen.SStr(currenth) << ")");
579  TraverseUncontrollableBackwards(rCAlph, rtransrel, forbidden, currenth);
580  // exit all loops over g transrel
581  titg = titg_end;
582  break;
583  }
584  FD_DF("mtcSupCon: incrementing g transrel");
585  ++titg;
586  }
587  // if specification leaves plant model emit warning
588  else {
589 #ifdef FAUDES_CHECKED
590  FD_WARN("mtcSupCon: transition " << rSpecGen.SStr(tith->X1) << "-"
591  << rSpecGen.EStr(tith->Ev) << "-" << rSpecGen.SStr(tith->X2)
592  << "in specification h not found in g");
593 #endif
594  FD_DF("mtcSupCon: incrementing h transrel");
595  ++tith;
596  }
597  }
598  // process other transitions not in h
599  while (titg != titg_end) {
600  FD_DF("mtcSupCon: asynchronous execution of event "
601  << rPlantGen.EStr(titg->Ev) << " in g at end of h");
602  FD_DF("mtcSupCon: actual g-transition: " << rPlantGen.SStr(titg->X1)
603  << "-" << rPlantGen.EStr(titg->Ev) << "-" << rPlantGen.SStr(titg->X2));
604  FD_DF("mtcSupCon: actual h-transition: end");
605  // if uncontrollable transition leaves specification
606  if (!rCAlph.Exists(titg->Ev)) {
607  FD_DF("mtcSupCon: asynchronous execution of uncontrollable event "
608  << rPlantGen.EStr(titg->Ev) << " in g");
609  FD_DF("mtcSupCon: TraverseUncontrollableBackwards(" << rPlantGen.SStr(currenth) << ")");
610  TraverseUncontrollableBackwards(rCAlph, rtransrel, forbidden, currenth);
611  // exit this loop
612  break;
613  }
614  FD_DF("mtcSupCon: incrementing g transrel");
615  ++titg;
616  }
617 #ifdef FAUDES_CHECKED
618  // process other transitions not in g
619  while (tith != tith_end) {
620  FD_WARN("mtcSupCon: transition " << rSpecGen.SStr(tith->X1) << "-"
621  << rSpecGen.EStr(tith->Ev) << "-" << rSpecGen.SStr(tith->X2)
622  << "in specification h not found in g");
623  FD_DF("mtcSupCon: incrementing h transrel");
624  ++tith;
625  }
626 #endif
627  discovered.Insert(currenth);
628  }
629 
630  // compute complete set of forbidden states
631  forbidden = rSpecGen.States() - ( discovered - forbidden );
632 
633  // remove forbidden states from stateset
634  rSpecGen.DelStates(forbidden);
635 }
636 
637 
638 
639 
640 } // namespace faudes
FD_WARN
#define FD_WARN(message)
Definition: cfl_definitions.h:85
FD_DF
#define FD_DF(message)
Definition: cfl_definitions.h:139
faudes::ExtType::Name
const std::string & Name(void) const
Definition: cfl_types.cpp:422
faudes::NameSet::Exists
bool Exists(const Idx &rIndex) const
Definition: cfl_nameset.cpp:438
faudes::TTransSet::Insert
bool Insert(const Transition &rTransition)
Definition: cfl_transset.h:1528
faudes::TTransSet< TransSort::X1EvX2 >::Iterator
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Definition: cfl_transset.h:273
faudes::TaGenerator::Clear
virtual void Clear(void)
Definition: cfl_agenerator.h:1067
faudes::TaGenerator::States
const TaStateSet< StateAttr > & States(void) const
Definition: cfl_agenerator.h:1363
faudes::TaGenerator::Alphabet
const TaEventSet< EventAttr > & Alphabet(void) const
Definition: cfl_agenerator.h:1358
faudes::TaGenerator::SetTransition
bool SetTransition(Idx x1, Idx ev, Idx x2)
Definition: cfl_agenerator.h:1197
faudes::TaGenerator::InjectAlphabet
void InjectAlphabet(const EventSet &rNewalphabet)
Definition: cfl_agenerator.h:1074
faudes::TcGenerator::ClrObservable
void ClrObservable(Idx index)
Definition: cfl_cgenerator.h:1021
faudes::TcGenerator::UncontrollableEvents
EventSet UncontrollableEvents(void) const
Definition: cfl_cgenerator.h:942
faudes::TcGenerator::ControllableEvents
EventSet ControllableEvents(void) const
Definition: cfl_cgenerator.h:930
faudes::TcGenerator::SetControllable
void SetControllable(Idx index)
Definition: cfl_cgenerator.h:882
faudes::TcGenerator::ForcibleEvents
EventSet ForcibleEvents(void) const
Definition: cfl_cgenerator.h:1161
faudes::TcGenerator::SetForcible
void SetForcible(Idx index)
Definition: cfl_cgenerator.h:1113
faudes::TcGenerator::UnobservableEvents
EventSet UnobservableEvents(void) const
Definition: cfl_cgenerator.h:1057
faudes::TmtcGenerator::InsColors
void InsColors(Idx stateIndex, const ColorSet &rColors)
Definition: mtc_generator.h:1042
faudes::TmtcGenerator::Colors
void Colors(ColorSet &rColors) const
Definition: mtc_generator.h:1182
faudes::Type::ToString
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
Definition: cfl_types.cpp:175
faudes::vGenerator::InitStatesBegin
StateSet::Iterator InitStatesBegin(void) const
Definition: cfl_generator.cpp:1147
faudes::vGenerator::InitStatesEmpty
bool InitStatesEmpty(void) const
Definition: cfl_generator.cpp:660
faudes::vGenerator::InitStates
const StateSet & InitStates(void) const
Definition: cfl_generator.cpp:1905
faudes::vGenerator::TransRelBegin
TransSet::Iterator TransRelBegin(void) const
Definition: cfl_generator.cpp:1064
faudes::vGenerator::ExistsState
bool ExistsState(Idx index) const
Definition: cfl_generator.cpp:1773
faudes::vGenerator::DelStates
void DelStates(const StateSet &rDelStates)
Definition: cfl_generator.cpp:1378
faudes::vGenerator::TransRelEnd
TransSet::Iterator TransRelEnd(void) const
Definition: cfl_generator.cpp:1069
faudes::vGenerator::IsDeterministic
bool IsDeterministic(void) const
Definition: cfl_generator.cpp:2333
faudes::vGenerator::EStr
std::string EStr(Idx index) const
Definition: cfl_generator.cpp:3885
faudes::vGenerator::Empty
bool Empty(void) const
Definition: cfl_generator.cpp:650
faudes::vGenerator::Size
Idx Size(void) const
Definition: cfl_generator.cpp:574
faudes::vGenerator::SStr
std::string SStr(Idx index) const
Definition: cfl_generator.cpp:3891
faudes::TBaseSet::Empty
bool Empty(void) const
Definition: cfl_baseset.h:1787
faudes::TBaseSet::Exists
bool Exists(const T &rElem) const
Definition: cfl_baseset.h:2180
faudes::mtcSupConClosed
void mtcSupConClosed(const MtcSystem &rPlantGen, const MtcSystem &rSpecGen, MtcSystem &rResGen)
Definition: mtc_supcon.cpp:130
faudes::mtcSupCon
void mtcSupCon(const MtcSystem &rPlantGen, const MtcSystem &rSpecGen, MtcSystem &rResGen)
Definition: mtc_supcon.cpp:41
mtc_supcon.h
faudes::Idx
uint32_t Idx
Definition: cfl_definitions.h:43
faudes::TraverseUncontrollableBackwards
void TraverseUncontrollableBackwards(const EventSet &rCAlph, TransSetX2EvX1 &rtransrel, StateSet &rCriticalStates, Idx current)
Definition: syn_supcon.cpp:847
faudes::mtcSupConParallel
void mtcSupConParallel(const MtcSystem &rPlantGen, const MtcSystem &rSpecGen, const EventSet &rUAlph, std::map< std::pair< Idx, Idx >, Idx > &rReverseCompositionMap, MtcSystem &rResGen)
Definition: mtc_supcon.cpp:220
faudes::ToStringInteger
std::string ToStringInteger(Int number)
Definition: cfl_utils.cpp:43
faudes::ComposedColorSet
void ComposedColorSet(const MtcSystem &rGen1, const Idx sidx1, ColorSet &rColors1, const MtcSystem &rGen2, const Idx sidx2, ColorSet &rColors2, ColorSet &composedSet)
Definition: mtc_parallel.cpp:213
faudes::mtcSupConUnchecked
void mtcSupConUnchecked(const MtcSystem &rPlantGen, const EventSet &rCAlph, MtcSystem &rSpecGen)
Definition: mtc_supcon.cpp:464
syn_include.h

libFAUDES 2.33h --- 2025.06.18 --- c++ api documentaion by doxygen

>>