13 FD_DIO(
"IsIoSystem("<< rIoSystem.
Name() <<
",...)");
18 rQErr.
Name(
"ErrorStates");
20 FD_DIO(
"IsIoSystem("<< rIoSystem.
Name() <<
",...): testing completeness");
23 StateSet::Iterator sit=acc.
Begin();
24 StateSet::Iterator sit_end=acc.
End();
25 for(;sit!=sit_end;sit++){
29 if(tit==tit_end) rQErr.
Insert(*sit);
34 FD_DIO(
"IsIoSystem("<< rIoSystem.
Name() <<
",...): not complete");
42 EventSet::Iterator eit_end= rIoSystem.
AlphabetEnd();
43 for(; eit != eit_end; ++eit) {
56 FD_DIO(
"IsIoSystem("<< rIoSystem.
Name() <<
",...): not a u-y partition of events");
59 for(; tit!=tit_end; tit++)
64 FD_DIO(
"IsIoSystem("<< rIoSystem.
Name() <<
",...): trivial partition");
68 FD_DIO(
"IsIoSystem("<< rIoSystem.
Name() <<
",...): i/o alternation");
72 for(; sit != sit_end; ++sit) {
76 for(; tit!=tit_end; tit++) {
87 for(; sit != sit_end; ++sit) {
93 while(!todo.empty()) {
94 const Idx current = todo.top();
96 bool uok = rQU.
Exists(current);
97 bool yok = rQY.
Exists(current);
101 for(; tit!=tit_end; tit++) {
106 if(!uok) rQErr.
Insert(current);
110 if(!yok) rQErr.
Insert(current);
125 bool res=
IsIoSystem(rIoSystem, QU, QY, QErr);
141 FD_DIO(
"IsInputLocallyFree("<< rIoSystem.
Name() <<
",...)");
150 FD_DIO(
"IsInputLocallyFree("<< rIoSystem.
Name() <<
",...)");
153 rQErr.
Name(
"ErrorStates");
158 StateSet::Iterator sit_end= rIoSystem.
StatesEnd();
159 for(; sit != sit_end; ++sit) {
164 for(; tit!=tit_end; tit++)
168 if(lsigu.
Empty())
continue;
170 if(lsigu == sigu)
continue;
175 return rQErr.
Empty();
181 FD_DIO(
"IsInputOmegaFree("<< rIoSystem.
Name() <<
",...)");
190 FD_DIO(
"IsInputOmegaFree("<< rIoSystem.
Name() <<
",...)");
195 FD_DIO(
"IsInputOmegaFree("<< rIoSystem.
Name() <<
",...): failed for locally free");
203 rQErr.
Name(
"ErrorStates");
208 FD_DIO(
"IsInputOmegaFree(...): iterate over good states");
210 StateSet::Iterator sit = rQErr.
Begin();
211 while(sit!=rQErr.
End()) {
213 StateSet::Iterator cit=sit++;
215 if(goodstates.
Exists(*cit))
continue;
220 if(tit==tit_end)
continue;
223 for(; tit!=tit_end; ++tit) {
224 if(goodstates.
Exists(tit->X2)) { exgood=
true;
continue; };
225 if(!yalph.
Exists(tit->Ev))
break;
228 if(exgood && (tit==tit_end)) {
229 FD_DIO(
"IsInputOmegaFree(): ins good state " << rIoSystem.
SStr(*cit));
241 FD_DIO(
"IsInputOmegaFree(): accessible <= good: passed");
246 FD_DIO(
"IsInputOmegaFree(): accessible <= good: failed");
258 FD_DIO(
"IoFreeInput("<< rGen.
Name() <<
",...)");
261 std::stringstream errstr;
262 errstr <<
"Input alphabet must be contained in generator alphabet";
263 throw Exception(
"IoFreeInput(..)", errstr.str(), 100);
269 EventSet::Iterator eit;
270 EventSet::Iterator eit_end;
273 StateSet::Iterator sit_end= rGen.
StatesEnd();
274 for(; sit != sit_end; ++sit) {
279 for(; tit!=tit_end; tit++)
282 if(lsigu.
Empty())
continue;
284 if(lsigu == rUAlph)
continue;
293 for(; eit!=eit_end; eit++) {
302 eit_end=rUAlph.
End();
303 for(; eit!=eit_end; eit++)
312 FD_DIO(
"RemoveIoDummyStates("<< rIoSystem.
Name() <<
",...)");
324 StateSet::Iterator sit_end= rIoSystem.
StatesEnd();
325 for(; sit != sit_end; ++sit) {
332 for(; tit!=tit_end; tit++) {
333 if(qsuc==0) qsuc=tit->X2;
334 if(qsuc!=tit->X2) { qunique=
false;
break;}
338 if(!qunique || qsuc==0)
continue;
340 if(!(lsig == sigy))
continue;
345 FD_DIO(
"RemoveIoDummyStates(): Candidates type 1 " << qerr1.
ToString());
346 FD_DIO(
"RemoveIoDummyStates(): Candidates type 2 " << qerr2.
ToString());
350 sit_end= qerr2.
End();
351 for(; sit != sit_end; ++sit) {
358 for(; tit!=tit_end; tit++) {
359 if(qsuc==0) qsuc=tit->X2;
360 if(qsuc!=tit->X2) { qunique=
false;
break;}
364 if(!qunique)
continue;
366 if(!qerr1.
Exists(qsuc))
continue;
368 if(!(lsig == sigu))
continue;
372 FD_DIO(
"RemoveIoDummyStates(): Candidates type 2 (approved) " << qerr2a.
ToString());
377 sit_end= qerr1.
End();
378 for(; sit != sit_end; ++sit) {
381 if(tit==tit_end) { qrm1.
Insert(*sit);
break;}
382 if(!qerr2a.
Exists(tit->X2)) { qrm1.
Insert(*sit);
break;}
386 sit = qerr2a.
Begin();
387 sit_end= qerr2a.
End();
388 for(; sit != sit_end; ++sit) {
391 if(tit==tit_end) { qrm2.
Insert(*sit);
break;}
401 for(; sit != sit_end; ++sit)
403 FD_DIO(
"RemoveIoDummyStates(): done");
422 FD_DIO(
"IoSynthesisClosed");
const std::string & Name(void) const
bool Exists(const Idx &rIndex) const
bool Insert(const Idx &rIndex)
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
bool InputEvent(Idx index) const
StateSet InputStates(void) const
StateSet OutputStates(void) const
StateSet ErrorStates(void) const
bool OutputEvent(Idx index) const
EventSet OutputEvents(void) const
EventSet InputEvents(void) const
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
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
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 Exists(const T &rElem) const
Iterator Begin(void) const
virtual bool Erase(const T &rElem)
virtual void EraseSet(const TBaseSet &rOtherSet)
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)
void IoSynthesisClosed(const IoSystem &rPlant, const Generator &rSpec, IoSystem &rSup)
void IoStatePartition(IoSystem &rIoSystem)
void IoSynthesis(const IoSystem &rPlant, const Generator &rSpec, IoSystem &rSup)