|
|
||||||
|
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("SupConNorm(" << 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 SupConNorm(rPlantGen,rPlantGen.ControllableEvents(),rPlantGen.ObservableEvents(),rSpecGen,*pResGen);
Definition: cfl_exception.h:118 Definition: cfl_indexset.h:78 Definition: cfl_nameset.h:70 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:394 TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator Definition: cfl_transset.h:273 const TaEventSet< EventAttr > & Alphabet(void) const Definition: cfl_agenerator.h:1358 Definition: cfl_cgenerator.h:76 EventSet ControllableEvents(void) const Definition: cfl_cgenerator.h:930 EventSet ObservableEvents(void) const Definition: cfl_cgenerator.h:1045 std::string ToString(const std::string &rLabel="", const Type *pContext=0) const Definition: cfl_types.cpp:175 Definition: cfl_generator.h:213 StateSet::Iterator InitStatesBegin(void) const Definition: cfl_generator.cpp:1147 bool SetTransition(Idx x1, Idx ev, Idx x2) Definition: cfl_generator.cpp:1623 const StateSet & MarkedStates(void) const Definition: cfl_generator.cpp:1910 virtual vGenerator & Assign(const Type &rSrc) Definition: cfl_generator.cpp:295 bool InitStatesEmpty(void) const Definition: cfl_generator.cpp:660 EventSet ActiveEventSet(Idx x1) const Definition: cfl_generator.cpp:1935 const StateSet & InitStates(void) const Definition: cfl_generator.cpp:1905 TransSet::Iterator TransRelBegin(void) const Definition: cfl_generator.cpp:1064 void ClrTransition(Idx x1, Idx ev, Idx x2) Definition: cfl_generator.cpp:1657 EventSet::Iterator AlphabetBegin(void) const Definition: cfl_generator.cpp:1044 void InjectMarkedStates(const StateSet &rNewMarkedStates) Definition: cfl_generator.cpp:1532 Idx MarkedStatesSize(void) const Definition: cfl_generator.cpp:640 StateSet::Iterator MarkedStatesBegin(void) const Definition: cfl_generator.cpp:1157 std::string TStr(const Transition &rTrans) const Definition: cfl_generator.cpp:3898 void DelStates(const StateSet &rDelStates) Definition: cfl_generator.cpp:1378 TransSet::Iterator TransRelEnd(void) const Definition: cfl_generator.cpp:1069 bool IsDeterministic(void) const Definition: cfl_generator.cpp:2333 StateSet::Iterator MarkedStatesEnd(void) const Definition: cfl_generator.cpp:1162 virtual void EventAttributes(const EventSet &rEventSet) Definition: cfl_generator.cpp:1727 bool StateNamesEnabled(void) const Definition: cfl_generator.cpp:996 EventSet::Iterator AlphabetEnd(void) const Definition: cfl_generator.cpp:1049 bool ExistsMarkedState(Idx index) const Definition: cfl_generator.cpp:1803 bool LanguageInclusion(const Generator &rGen1, const Generator &rGen2) Definition: cfl_regular.cpp:837 void Product(const Generator &rGen1, const Generator &rGen2, Generator &rResGen) Definition: cfl_parallel.cpp:517 void LanguageDifference(const Generator &rGen1, const Generator &rGen2, Generator &rResGen) Definition: cfl_regular.cpp:529 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 SupConNorm(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 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 bool SupClosed(const Generator &rK, Generator &rResult) Definition: syn_supnorm.cpp:419 void SupPrefixClosed(const Generator &rK, Generator &rResult) Definition: syn_supnorm.cpp:729 libFAUDES 2.33h --- 2025.06.18 --- c++ api documentaion by doxygen |