ios_algorithms.cpp
Go to the documentation of this file.
1 #include "ios_algorithms.h"
2 #include "syn_include.h"
3 #include "omg_include.h"
4 
5 namespace faudes {
6 
7 // IsIoSystem() implementation
8 bool IsIoSystem(const IoSystem& rIoSystem,
9  StateSet& rQU,
10  StateSet& rQY,
11  StateSet& rQErr)
12 {
13  FD_DIO("IsIoSystem("<< rIoSystem.Name() << ",...)");
14  // prepare result
15  rQU.Clear();
16  rQY.Clear();
17  rQErr.Clear();
18  rQErr.Name("ErrorStates");
19  // completeness (iterate over accessible states only)
20  FD_DIO("IsIoSystem("<< rIoSystem.Name() << ",...): testing completeness");
21  StateSet acc = rIoSystem.AccessibleSet();
22  StateSet coacc = rIoSystem.CoaccessibleSet();
23  StateSet::Iterator sit=acc.Begin();
24  StateSet::Iterator sit_end=acc.End();
25  for(;sit!=sit_end;sit++){
26  // cannot extend
27  TransSet::Iterator tit=rIoSystem.TransRelBegin(*sit);
28  TransSet::Iterator tit_end=rIoSystem.TransRelEnd(*sit);
29  if(tit==tit_end) rQErr.Insert(*sit);
30  // not coreachable
31  if(!coacc.Exists(*sit)) rQErr.Insert(*sit);
32  }
33  if(!rQErr.Empty()) {
34  FD_DIO("IsIoSystem("<< rIoSystem.Name() << ",...): not complete");
35  return false;
36  }
37  // insist in a u-y partition
38  EventSet errev;
39  bool hasu=false;
40  bool hasy=false;
41  EventSet::Iterator eit = rIoSystem.AlphabetBegin();
42  EventSet::Iterator eit_end= rIoSystem.AlphabetEnd();
43  for(; eit != eit_end; ++eit) {
44  if(rIoSystem.InputEvent(*eit))
45  hasu=true;
46  if(rIoSystem.InputEvent(*eit))
47  hasy=true;
48  if(rIoSystem.InputEvent(*eit))
49  if(rIoSystem.OutputEvent(*eit))
50  errev.Insert(*eit);
51  if(!rIoSystem.InputEvent(*eit))
52  if(!rIoSystem.OutputEvent(*eit))
53  errev.Insert(*eit);
54  }
55  if(!errev.Empty()) {
56  FD_DIO("IsIoSystem("<< rIoSystem.Name() << ",...): not a u-y partition of events");
57  TransSet::Iterator tit=rIoSystem.TransRelBegin();
58  TransSet::Iterator tit_end=rIoSystem.TransRelEnd();
59  for(; tit!=tit_end; tit++)
60  if(errev.Exists(tit->Ev)) rQErr.Insert(tit->X1);
61  return false;
62  }
63  if(!hasu || !hasy) {
64  FD_DIO("IsIoSystem("<< rIoSystem.Name() << ",...): trivial partition");
65  return false;
66  }
67  // io-alternation: fill todo stack with initial states
68  FD_DIO("IsIoSystem("<< rIoSystem.Name() << ",...): i/o alternation");
69  std::stack<Idx> todo;
70  sit = rIoSystem.InitStatesBegin();
71  sit_end= rIoSystem.InitStatesEnd();
72  for(; sit != sit_end; ++sit) {
73  // figure type of initial state
74  TransSet::Iterator tit=rIoSystem.TransRelBegin(*sit);
75  TransSet::Iterator tit_end=rIoSystem.TransRelEnd(*sit);
76  for(; tit!=tit_end; tit++) {
77  if(rIoSystem.InputEvent(tit->Ev)) rQU.Insert(*sit);
78  if(rIoSystem.OutputEvent(tit->Ev)) rQY.Insert(*sit);
79  }
80  // push
81  todo.push(*sit);
82  }
83  // io-alternation: multiple initialstates are fine, but must be of same type.
84  if(!rQU.Empty() && !rQY.Empty()) {
85  sit = rIoSystem.InitStatesBegin();
86  sit_end= rIoSystem.InitStatesEnd();
87  for(; sit != sit_end; ++sit) {
88  rQErr.Insert(*sit);
89  return false;
90  }
91  }
92  // io-alternation: process stack
93  while(!todo.empty()) {
94  const Idx current = todo.top();
95  todo.pop();
96  bool uok = rQU.Exists(current);
97  bool yok = rQY.Exists(current);
98  // iterate all transitions
99  TransSet::Iterator tit=rIoSystem.TransRelBegin(current);
100  TransSet::Iterator tit_end=rIoSystem.TransRelEnd(current);
101  for(; tit!=tit_end; tit++) {
102  if(!rQY.Exists(tit->X2) && !rQU.Exists(tit->X2))
103  todo.push(tit->X2);
104  if(rIoSystem.InputEvent(tit->Ev)) {
105  rQY.Insert(tit->X2);
106  if(!uok) rQErr.Insert(current);
107  }
108  if(rIoSystem.OutputEvent(tit->Ev)) {
109  rQU.Insert(tit->X2);
110  if(!yok) rQErr.Insert(current);
111  }
112  }
113  }
114  if(!rQErr.Empty()) {
115  return false;
116  }
117  // done
118  return true;
119 }
120 
121 
122 // IsIoSystem wrapper function
123 bool IsIoSystem(IoSystem& rIoSystem) {
124  StateSet QU,QY, QErr;
125  bool res= IsIoSystem(rIoSystem, QU, QY, QErr);
126  rIoSystem.InputStates(QU);
127  rIoSystem.OutputStates(QY);
128  rIoSystem.ErrorStates(QErr);
129  return res;
130 }
131 
132 
133 // rti function interface
134 void IoStatePartition(IoSystem& rIoSystem) {
135  IsIoSystem(rIoSystem);
136 }
137 
138 
139 // IsInputLocallyFree wrapper function
140 bool IsInputLocallyFree(IoSystem& rIoSystem) {
141  FD_DIO("IsInputLocallyFree("<< rIoSystem.Name() << ",...)");
142  StateSet QErr;
143  bool res=IsInputLocallyFree(rIoSystem, QErr);
144  rIoSystem.ErrorStates(QErr);
145  return res;
146 }
147 
148 // IsInputLocallyFree implementation
149 bool IsInputLocallyFree(const IoSystem& rIoSystem, StateSet& rQErr) {
150  FD_DIO("IsInputLocallyFree("<< rIoSystem.Name() << ",...)");
151  // prepare result
152  rQErr.Clear();
153  rQErr.Name("ErrorStates");
154  // have set of all input events
155  EventSet sigu=rIoSystem.InputEvents();
156  // test all states
157  StateSet::Iterator sit = rIoSystem.StatesBegin();
158  StateSet::Iterator sit_end= rIoSystem.StatesEnd();
159  for(; sit != sit_end; ++sit) {
160  // get all enabled inputs
161  EventSet lsigu;
162  TransSet::Iterator tit=rIoSystem.TransRelBegin(*sit);
163  TransSet::Iterator tit_end=rIoSystem.TransRelEnd(*sit);
164  for(; tit!=tit_end; tit++)
165  if(rIoSystem.InputEvent(tit->Ev)) lsigu.Insert(tit->Ev);
166  //FD_DIO("DUMP " << rIoSystem.StateName(*sit) << " "<< lsigu.ToString());
167  // no inputs? fine
168  if(lsigu.Empty()) continue;
169  // all inputs? fine
170  if(lsigu == sigu) continue;
171  // error
172  rQErr.Insert(*sit);
173  //FD_DIO("DUMP " << *sit << " " << rQErr.ToString());
174  }
175  return rQErr.Empty();
176 }
177 
178 
179 // IsInputOmegaFree wrapper function
180 bool IsInputOmegaFree(IoSystem& rIoSystem) {
181  FD_DIO("IsInputOmegaFree("<< rIoSystem.Name() << ",...)");
182  StateSet QErr;
183  bool res=IsInputOmegaFree(rIoSystem, QErr);
184  rIoSystem.ErrorStates(QErr);
185  return res;
186 }
187 
188 // Is InputOmegaFree implementation
189 bool IsInputOmegaFree(const IoSystem& rIoSystem, StateSet& rQErr) {
190  FD_DIO("IsInputOmegaFree("<< rIoSystem.Name() << ",...)");
191 
192  // test for locally free input first
193  rQErr.Clear();
194  if(!IsInputLocallyFree(rIoSystem,rQErr)) {
195  FD_DIO("IsInputOmegaFree("<< rIoSystem.Name() << ",...): failed for locally free");
196  return false;
197  }
198 
199  // prepare good state iteration
200  StateSet goodstates=rIoSystem.MarkedStates();
201  EventSet yalph=rIoSystem.OutputEvents();
202  rQErr=rIoSystem.AccessibleSet()-goodstates;
203  rQErr.Name("ErrorStates");
204 
205  // control to good states by choosing strategic y-events
206  while(true) {
207  // test individual states
208  FD_DIO("IsInputOmegaFree(...): iterate over good states");
209  bool found=false;
210  StateSet::Iterator sit = rQErr.Begin();
211  while(sit!=rQErr.End()) {
212  // pre-increment
213  StateSet::Iterator cit=sit++;
214  // goodstate anyway
215  if(goodstates.Exists(*cit)) continue;
216  // test transitions
217  TransSet::Iterator tit = rIoSystem.TransRelBegin(*cit);
218  TransSet::Iterator tit_end = rIoSystem.TransRelEnd(*cit);
219  // no transitions at all: no chance
220  if(tit==tit_end) continue;
221  // iterate successors
222  bool exgood=false;
223  for(; tit!=tit_end; ++tit) {
224  if(goodstates.Exists(tit->X2)) { exgood=true; continue; };
225  if(!yalph.Exists(tit->Ev)) break; // break on not-good successor with non-y-event (aka u-event)
226  }
227  // succes: good successor exists and all not-good successors are y-events [rev tmoor 201507]
228  if(exgood && (tit==tit_end)) {
229  FD_DIO("IsInputOmegaFree(): ins good state " << rIoSystem.SStr(*cit));
230  goodstates.Insert(*cit);
231  rQErr.Erase(cit);
232  found=true;
233  }
234  }
235  // exit
236  if(!found) break;
237  };
238 
239  // errorstates
240  if(rQErr.Empty()) {
241  FD_DIO("IsInputOmegaFree(): accessible <= good: passed");
242  return true;
243  }
244 
245  // fail
246  FD_DIO("IsInputOmegaFree(): accessible <= good: failed");
247  return false;
248 }
249 
250 
251 // IoFreeInput() wrapper
252 void IoFreeInput(IoSystem& rIoSystem) {
253  IoFreeInput(rIoSystem,rIoSystem.InputEvents());
254 }
255 
256 // IoFreeInput()
257 void IoFreeInput(Generator& rGen, const EventSet& rUAlph) {
258  FD_DIO("IoFreeInput("<< rGen.Name() << ",...)");
259  // test alphabet
260  if(!(rUAlph <= rGen.Alphabet())){
261  std::stringstream errstr;
262  errstr << "Input alphabet must be contained in generator alphabet";
263  throw Exception("IoFreeInput(..)", errstr.str(), 100);
264  }
265  // prepare error states
266  Idx qyerr=0;
267  Idx querr=0;
268  // declare some local vars
269  EventSet::Iterator eit;
270  EventSet::Iterator eit_end;
271  // test all states
272  StateSet::Iterator sit = rGen.StatesBegin();
273  StateSet::Iterator sit_end= rGen.StatesEnd();
274  for(; sit != sit_end; ++sit) {
275  // get all enabled inputs
276  EventSet lsigu;
277  TransSet::Iterator tit=rGen.TransRelBegin(*sit);
278  TransSet::Iterator tit_end=rGen.TransRelEnd(*sit);
279  for(; tit!=tit_end; tit++)
280  if(rUAlph.Exists(tit->Ev)) lsigu.Insert(tit->Ev);
281  // no inputs? fine
282  if(lsigu.Empty()) continue;
283  // all inputs? fine
284  if(lsigu == rUAlph) continue;
285  // no error states yet? insert them
286  if(qyerr==0) {
287  // todo: be smart in state names when enabled
288  qyerr = rGen.InsMarkedState();
289  querr = rGen.InsMarkedState();
290  // enable all transition
291  eit=rGen.Alphabet().Begin();
292  eit_end=rGen.Alphabet().End();
293  for(; eit!=eit_end; eit++) {
294  if(rUAlph.Exists(*eit))
295  rGen.SetTransition(querr,*eit,qyerr);
296  else
297  rGen.SetTransition(qyerr,*eit,querr);
298  }
299  }
300  // fix the state at hand
301  eit=rUAlph.Begin();
302  eit_end=rUAlph.End();
303  for(; eit!=eit_end; eit++)
304  if(!lsigu.Exists(*eit))
305  rGen.SetTransition(*sit,*eit,qyerr);
306  // continue with next state
307  }
308 }
309 
310 // IoRemoveDummyStates
311 void RemoveIoDummyStates(IoSystem& rIoSystem) {
312  FD_DIO("RemoveIoDummyStates("<< rIoSystem.Name() << ",...)");
313  // have set of all input/output events
314  EventSet sigu=rIoSystem.InputEvents();
315  EventSet sigy=rIoSystem.OutputEvents();
316  // have results
317  StateSet qerr1; // a) find all outputs to unique successor
318  StateSet qerr2; // b) collect successors from a)
319  StateSet qerr2a; // c) from qerr2 only keep all with unique successor
320  StateSet qerr; // d) restrict candidates to cyclic behaviour
321  // find states with all outputs leading to the same successor
322  // record as type 1 candidate
323  StateSet::Iterator sit = rIoSystem.StatesBegin();
324  StateSet::Iterator sit_end= rIoSystem.StatesEnd();
325  for(; sit != sit_end; ++sit) {
326  // get all enabled events, track for unique successor
327  EventSet lsig;
328  Idx qsuc=0;
329  bool qunique=true;
330  TransSet::Iterator tit=rIoSystem.TransRelBegin(*sit);
331  TransSet::Iterator tit_end=rIoSystem.TransRelEnd(*sit);
332  for(; tit!=tit_end; tit++) {
333  if(qsuc==0) qsuc=tit->X2;
334  if(qsuc!=tit->X2) { qunique=false; break;}
335  lsig.Insert(tit->Ev);
336  }
337  // non unique successor? discard
338  if(!qunique || qsuc==0) continue;
339  // outputs not enabled? discard
340  if(!(lsig == sigy)) continue;
341  // record candidate
342  qerr1.Insert(*sit);
343  qerr2.Insert(qsuc);
344  }
345  FD_DIO("RemoveIoDummyStates(): Candidates type 1 " << qerr1.ToString());
346  FD_DIO("RemoveIoDummyStates(): Candidates type 2 " << qerr2.ToString());
347  // only keep type 2 candidates with all inputs enabled and
348  // leading to a type 1 candidate
349  sit = qerr2.Begin();
350  sit_end= qerr2.End();
351  for(; sit != sit_end; ++sit) {
352  // get all enabled events, track for unique successor
353  EventSet lsig;
354  Idx qsuc=0;
355  bool qunique=true;
356  TransSet::Iterator tit=rIoSystem.TransRelBegin(*sit);
357  TransSet::Iterator tit_end=rIoSystem.TransRelEnd(*sit);
358  for(; tit!=tit_end; tit++) {
359  if(qsuc==0) qsuc=tit->X2;
360  if(qsuc!=tit->X2) { qunique=false; break;}
361  lsig.Insert(tit->Ev);
362  }
363  // non unique successor? discard
364  if(!qunique) continue;
365  // successor not in candidates? discard
366  if(!qerr1.Exists(qsuc)) continue;
367  // inputs not enabled? discard
368  if(!(lsig == sigu)) continue;
369  // record candidate
370  qerr2a.Insert(*sit);
371  }
372  FD_DIO("RemoveIoDummyStates(): Candidates type 2 (approved) " << qerr2a.ToString());
373  // only keep loops
374  while(1) {
375  StateSet qrm1;
376  sit = qerr1.Begin();
377  sit_end= qerr1.End();
378  for(; sit != sit_end; ++sit) {
379  TransSet::Iterator tit=rIoSystem.TransRelBegin(*sit);
380  TransSet::Iterator tit_end=rIoSystem.TransRelEnd(*sit);
381  if(tit==tit_end) { qrm1.Insert(*sit); break;}
382  if(!qerr2a.Exists(tit->X2)) { qrm1.Insert(*sit); break;}
383  }
384  qerr1.EraseSet(qrm1);
385  StateSet qrm2;
386  sit = qerr2a.Begin();
387  sit_end= qerr2a.End();
388  for(; sit != sit_end; ++sit) {
389  TransSet::Iterator tit=rIoSystem.TransRelBegin(*sit);
390  TransSet::Iterator tit_end=rIoSystem.TransRelEnd(*sit);
391  if(tit==tit_end) { qrm2.Insert(*sit); break;}
392  if(!qerr1.Exists(tit->X2)) { qrm2.Insert(*sit); break;}
393  }
394  qerr2a.EraseSet(qrm2);
395  if(qrm1.Empty() && qrm2.Empty()) break;
396  }
397  qerr=qerr1 + qerr2;
398  FD_DIO("RemoveIoDummyStates(): Dummy states" << qerr.ToString());
399  sit = qerr.Begin();
400  sit_end= qerr.End();
401  for(; sit != sit_end; ++sit)
402  rIoSystem.DelState(*sit);
403  FD_DIO("RemoveIoDummyStates(): done");
404 }
405 
406 // IoSynthesis(rPlant,rSpec,rSup,rErrorStates)
407 void IoSynthesis(const IoSystem& rPlant, const Generator& rSpec, IoSystem& rSup) {
408  FD_DIO("IoSynthesis");
409 
410  // synthesis
411  EventSet ualph = rPlant.InputEvents();
412  EventSet yalph = rPlant.OutputEvents();
413  SupBuechiCon(rPlant,ualph,rSpec,rSup) ;
414 
415  // fix event attributes
416  rSup.InputEvents(yalph);
417  rSup.OutputEvents(ualph);
418 }
419 
420 // IoSynthesisClosed(rPlant,rSpec,rSup,rErrorStates)
421 void IoSynthesisClosed(const IoSystem& rPlant, const Generator& rSpec, IoSystem& rSup) {
422  FD_DIO("IoSynthesisClosed");
423 
424  // synthesis
425  EventSet ualph = rPlant.InputEvents();
426  EventSet yalph = rPlant.OutputEvents();
427  SupConCmplClosed(rPlant,ualph,rSpec,rSup) ;
428 
429  // fix event attributes
430  rSup.InputEvents(yalph);
431  rSup.OutputEvents(ualph);
432 }
433 
434 
435 }// end: namespace faudes
const std::string & Name(void) const
Definition: cfl_types.cpp:422
bool Exists(const Idx &rIndex) const
bool Insert(const Idx &rIndex)
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Definition: cfl_transset.h:273
bool InputEvent(Idx index) const
Definition: ios_system.h:967
StateSet InputStates(void) const
Definition: ios_system.h:1100
StateSet OutputStates(void) const
Definition: ios_system.h:1023
StateSet ErrorStates(void) const
Definition: ios_system.h:1179
bool OutputEvent(Idx index) const
Definition: ios_system.h:890
EventSet OutputEvents(void) const
Definition: ios_system.h:870
EventSet InputEvents(void) const
Definition: ios_system.h:946
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
Definition: cfl_types.cpp:175
StateSet::Iterator StatesBegin(void) const
StateSet::Iterator InitStatesBegin(void) const
bool SetTransition(Idx x1, Idx ev, Idx x2)
const StateSet & MarkedStates(void) const
const EventSet & Alphabet(void) const
TransSet::Iterator TransRelBegin(void) const
EventSet::Iterator AlphabetBegin(void) const
StateSet AccessibleSet(void) const
bool DelState(Idx index)
StateSet::Iterator StatesEnd(void) const
TransSet::Iterator TransRelEnd(void) const
StateSet::Iterator InitStatesEnd(void) const
EventSet::Iterator AlphabetEnd(void) const
StateSet CoaccessibleSet(void) const
std::string SStr(Idx index) const
bool Empty(void) const
Definition: cfl_baseset.h:1787
bool Exists(const T &rElem) const
Definition: cfl_baseset.h:2180
virtual void Clear(void)
Definition: cfl_baseset.h:1962
Iterator End(void) const
Definition: cfl_baseset.h:1956
Iterator Begin(void) const
Definition: cfl_baseset.h:1951
virtual bool Erase(const T &rElem)
Definition: cfl_baseset.h:2084
virtual void EraseSet(const TBaseSet &rOtherSet)
Definition: cfl_baseset.h:2107
void RemoveIoDummyStates(IoSystem &rIoSystem)
bool IsInputOmegaFree(IoSystem &rIoSystem)
bool IsInputLocallyFree(IoSystem &rIoSystem)
bool IsIoSystem(const IoSystem &rIoSystem, StateSet &rQU, StateSet &rQY, StateSet &rQErr)
void IoFreeInput(IoSystem &rIoSystem)
void SupBuechiCon(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
void SupConCmplClosed(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
Definition: syn_supcmpl.cpp:45
#define FD_DIO(message)
uint32_t Idx
void IoSynthesisClosed(const IoSystem &rPlant, const Generator &rSpec, IoSystem &rSup)
void IoStatePartition(IoSystem &rIoSystem)
void IoSynthesis(const IoSystem &rPlant, const Generator &rSpec, IoSystem &rSup)

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