|
|
||||||
|
syn_supnorm.cpp
Go to the documentation of this file.
189 // all marked states become eqivalent -> switch transitions leading to marked states to one remaining marked state
217 // delete all but the remaining marked state (note: by doing so, also corresp. transitions are cleared.)
400 FD_DF("SupConNormNB(" << rL.Name() << "," << rK.Name() << "): #" << Ki.Size() << " m#" << Ki.MarkedStatesSize());
499 FD_DF("SupConNormClosedUnchecked(" << &rSupCandGen << "," << &rPlantGen << "): until fixpoint #" << rSupCandGen.Size());
536 FD_DF("SupConNormClosed: pop: (" << rPlantGen.SStr(current.q) << "|" << rSupCandGen.SStr(current.x) << ")");
546 EventSet disabled = rPlantGen.ActiveEventSet(current.q) - rSupCandGen.ActiveEventSet(current.x);
585 // increment case B: increment H transitions for events disabled by Hobs (when we disabled events in Hobs)
589 // increment case C: increment Hobs transitions for events disabled by H (for removed critical states))
607 // increment case B: increment H transitions for events disabled by Hobs (when we disabled events in Hobs)
695 SupConNormClosed(rPlantGen,rPlantGen.ControllableEvents(),rPlantGen.ObservableEvents(),rSpecGen,*pResGen);
718 SupConNormNB(rPlantGen,rPlantGen.ControllableEvents(),rPlantGen.ObservableEvents(),rSpecGen,*pResGen);
Definition: cfl_exception.h:118 Definition: cfl_indexset.h:78 Definition: cfl_nameset.h:69 Definition: syn_supnorm.cpp:455 bool operator<(const SNOState &other) const Definition: syn_supnorm.cpp:464 SNOState(const Idx &rq, const Idx &rx, const bool &rz) Definition: syn_supnorm.cpp:459 Definition: cfl_baseset.h:396 TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator Definition: cfl_transset.h:273 const TaEventSet< EventAttr > & Alphabet(void) const Definition: cfl_agenerator.h:1360 Definition: cfl_cgenerator.h:278 EventSet ControllableEvents(void) const Definition: cfl_cgenerator.h:1132 EventSet ObservableEvents(void) const Definition: cfl_cgenerator.h:1247 std::string ToString(const std::string &rLabel="", const Type *pContext=0) const Definition: cfl_types.cpp:170 Definition: cfl_generator.h:213 StateSet::Iterator InitStatesBegin(void) const Definition: cfl_generator.cpp:1150 bool SetTransition(Idx x1, Idx ev, Idx x2) Definition: cfl_generator.cpp:1626 const StateSet & MarkedStates(void) const Definition: cfl_generator.cpp:1913 virtual vGenerator & Assign(const Type &rSrc) Definition: cfl_generator.cpp:287 bool InitStatesEmpty(void) const Definition: cfl_generator.cpp:663 EventSet ActiveEventSet(Idx x1) const Definition: cfl_generator.cpp:1938 const StateSet & InitStates(void) const Definition: cfl_generator.cpp:1908 TransSet::Iterator TransRelBegin(void) const Definition: cfl_generator.cpp:1067 void ClrTransition(Idx x1, Idx ev, Idx x2) Definition: cfl_generator.cpp:1660 EventSet::Iterator AlphabetBegin(void) const Definition: cfl_generator.cpp:1047 void InjectMarkedStates(const StateSet &rNewMarkedStates) Definition: cfl_generator.cpp:1535 Idx MarkedStatesSize(void) const Definition: cfl_generator.cpp:643 StateSet::Iterator MarkedStatesBegin(void) const Definition: cfl_generator.cpp:1160 std::string TStr(const Transition &rTrans) const Definition: cfl_generator.cpp:3841 void DelStates(const StateSet &rDelStates) Definition: cfl_generator.cpp:1381 TransSet::Iterator TransRelEnd(void) const Definition: cfl_generator.cpp:1072 bool IsDeterministic(void) const Definition: cfl_generator.cpp:2367 StateSet::Iterator MarkedStatesEnd(void) const Definition: cfl_generator.cpp:1165 virtual void EventAttributes(const EventSet &rEventSet) Definition: cfl_generator.cpp:1730 bool StateNamesEnabled(void) const Definition: cfl_generator.cpp:999 EventSet::Iterator AlphabetEnd(void) const Definition: cfl_generator.cpp:1052 bool ExistsMarkedState(Idx index) const Definition: cfl_generator.cpp:1806 bool LanguageInclusion(const Generator &rGen1, const Generator &rGen2) Definition: cfl_regular.cpp:830 void Product(const Generator &rGen1, const Generator &rGen2, Generator &rResGen) Definition: cfl_parallel.cpp:470 void LanguageDifference(const Generator &rGen1, const Generator &rGen2, Generator &rResGen) Definition: cfl_regular.cpp:522 void LanguageIntersection(const Generator &rGen1, const Generator &rGen2, Generator &rResGen) Definition: cfl_regular.cpp:188 void Project(const Generator &rGen, const EventSet &rProjectAlphabet, Generator &rResGen) Definition: cfl_project.cpp:1349 void InvProject(Generator &rGen, const EventSet &rProjectAlphabet) Definition: cfl_project.cpp:1479 bool SupNorm(const Generator &rL, const EventSet &rOAlph, const Generator &rK, Generator &rResult) Definition: syn_supnorm.cpp:234 bool IsNormal(const Generator &rL, const EventSet &rOAlph, const Generator &rK) Definition: syn_supnorm.cpp:104 void SupConNormClosed(const Generator &rL, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rK, Generator &rResult) Definition: syn_supnorm.cpp:336 void SupConNormNB(const Generator &rL, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rK, Generator &rResult) Definition: syn_supnorm.cpp:376 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) Definition: syn_supnorm.cpp:287 Definition: cfl_agenerator.h:43 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) Definition: syn_supnorm.cpp:480 bool SupPrefixClosed(const Generator &rK, Generator &rResult) Definition: syn_supnorm.cpp:419 void ConcatenateFullLanguage(Generator &rGen) Definition: syn_supnorm.cpp:153 void ControlProblemConsistencyCheck(const GeneratorVector &rPlantGenVec, const EventSet &rConAlph, const GeneratorVector &rSpecGenVec) Definition: syn_compsyn.cpp:1301 libFAUDES 2.33b --- 2025.05.07 --- c++ api documentaion by doxygen |