|
|
||||||
|
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);
#define FD_WPC(cntnow, contdone, message) Application callback: optional write progress report to console or application, incl count Definition: cfl_definitions.h:107 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 Iterator class for high-level api to TBaseSet. Definition: cfl_baseset.h:387 Iterator BeginByX2(Idx x2) const Iterator to first Transition specified by successor state x2. Definition: cfl_transset.h:1385 Iterator EndByX2(Idx x2) const Iterator to first Transition after specified successor state x2. Definition: cfl_transset.h:1396 TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator Iterator on transition. Definition: cfl_transset.h:269 const TaEventSet< EventAttr > & Alphabet(void) const Return const reference to alphabet. Definition: cfl_agenerator.h:1358 EventSet ControllableEvents(void) const Get EventSet with controllable events. Definition: cfl_cgenerator.h:1124 EventSet ObservableEvents(void) const Get EventSet with observable events. Definition: cfl_cgenerator.h:1239 std::string ToString(const std::string &rLabel="", const Type *pContext=0) const Write configuration data to a string. Definition: cfl_types.cpp:169 StateSet::Iterator InitStatesBegin(void) const Iterator to Begin() of mInitStates. Definition: cfl_generator.cpp:1150 const TransSet & TransRel(void) const Return reference to transition relation. Definition: cfl_generator.cpp:1888 bool SetTransition(Idx x1, Idx ev, Idx x2) Add a transition to generator by indices. Definition: cfl_generator.cpp:1626 const StateSet & MarkedStates(void) const Return const ref of marked states. Definition: cfl_generator.cpp:1913 const EventSet & Alphabet(void) const Return const reference to alphabet. Definition: cfl_generator.cpp:1878 virtual void Move(vGenerator &rGen) Destructive copy to other vGenerator. Definition: cfl_generator.cpp:333 virtual vGenerator & Assign(const Type &rSrc) Copy from other faudes type. Definition: cfl_generator.cpp:287 bool InitStatesEmpty(void) const Check if set of initial states are empty. Definition: cfl_generator.cpp:663 EventSet ActiveEventSet(Idx x1) const Return active event set at state x1. Definition: cfl_generator.cpp:1938 const StateSet & InitStates(void) const Const ref to initial states. Definition: cfl_generator.cpp:1908 TransSet::Iterator TransRelBegin(void) const Iterator to Begin() of transition relation. Definition: cfl_generator.cpp:1067 void ClrTransition(Idx x1, Idx ev, Idx x2) Remove a transition by indices. Definition: cfl_generator.cpp:1660 void ClearStates(void) Clear all states and transitions, maintain alphabet. Definition: cfl_generator.cpp:624 EventSet::Iterator AlphabetBegin(void) const Iterator to Begin() of alphabet. Definition: cfl_generator.cpp:1047 void InjectMarkedStates(const StateSet &rNewMarkedStates) Replace mMarkedStates with StateSet given as parameter without consistency checks. Definition: cfl_generator.cpp:1535 StateSet::Iterator MarkedStatesBegin(void) const Iterator to Begin() of mMarkedStates. Definition: cfl_generator.cpp:1160 std::string TStr(const Transition &rTrans) const Return pretty printable transition (eg for debugging) Definition: cfl_generator.cpp:3841 void DelStates(const StateSet &rDelStates) Delete a set of states Cleans mpStates, mInitStates, mMarkedStates, mpTransrel, and mpStateSymboltabl... Definition: cfl_generator.cpp:1381 TransSet::Iterator TransRelEnd(void) const Iterator to End() of transition relation. Definition: cfl_generator.cpp:1072 bool IsDeterministic(void) const Check if generator is deterministic. Definition: cfl_generator.cpp:2367 std::string EStr(Idx index) const Pretty printable event name for index (eg for debugging). Definition: cfl_generator.cpp:3828 StateSet::Iterator MarkedStatesEnd(void) const Iterator to End() of mMarkedStates. Definition: cfl_generator.cpp:1165 void SetMarkedState(Idx index) Set an existing state as marked state by index. Definition: cfl_generator.cpp:1507 Idx InsInitState(void) Create new anonymous state and set as initial state. Definition: cfl_generator.cpp:1287 virtual void EventAttributes(const EventSet &rEventSet) Set attributes for existing events. Definition: cfl_generator.cpp:1730 bool StateNamesEnabled(void) const Whether libFAUEDS functions are requested to generate state names. Definition: cfl_generator.cpp:999 EventSet::Iterator AlphabetEnd(void) const Iterator to End() of alphabet. Definition: cfl_generator.cpp:1052 std::string SStr(Idx index) const Return pretty printable state name for index (eg for debugging) Definition: cfl_generator.cpp:3834 bool ExistsMarkedState(Idx index) const Test existence of state in mMarkedStates. Definition: cfl_generator.cpp:1806 bool LanguageInclusion(const Generator &rGen1, const Generator &rGen2) Test language inclusion, Lm1<=Lm2. Definition: cfl_regular.cpp:815 void Product(const Generator &rGen1, const Generator &rGen2, Generator &rResGen) Product composition. Definition: cfl_parallel.cpp:418 bool IsEmptyLanguage(const Generator &rGen) Test for Empty language Lm(G)=={}. Definition: cfl_regular.cpp:806 void LanguageDifference(const Generator &rGen1, const Generator &rGen2, Generator &rResGen) Language difference (set-theoretic difference). Definition: cfl_regular.cpp:507 void LanguageIntersection(const Generator &rGen1, const Generator &rGen2, Generator &rResGen) Language intersection. Definition: cfl_regular.cpp:188 void Project(const Generator &rGen, const EventSet &rProjectAlphabet, Generator &rResGen) Deterministic projection. Definition: cfl_project.cpp:1349 void InvProject(Generator &rGen, const EventSet &rProjectAlphabet) Inverse projection. Definition: cfl_project.cpp:1479 bool SupNorm(const Generator &rL, const EventSet &rOAlph, const Generator &rK, Generator &rResult) SupNorm: compute supremal normal sublanguage. Definition: syn_supnorm.cpp:234 bool IsNormal(const Generator &rL, const EventSet &rOAlph, const Generator &rK) IsNormal: checks normality of a language K generated by rK wrt a language L generated by rL and the s... Definition: syn_supnorm.cpp:104 void SupConNormClosed(const Generator &rL, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rK, Generator &rResult) SupConNormClosed: compute supremal controllable, normal and closed sublanguage. Definition: syn_supnorm.cpp:336 void SupConNormNB(const Generator &rL, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rK, Generator &rResult) SupConNormNB: compute supremal controllable and normal sublanguage. Definition: syn_supnorm.cpp:376 void SupConClosed(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen) Supremal Controllable and Closed Sublanguage. Definition: syn_supcon.cpp:778 bool SupNormClosed(const Generator &rL, const EventSet &rOAlph, const Generator &rK, Generator &rResult) SupNormClosed - compute supremal normal and closed sublanguage. Definition: syn_supnorm.cpp:287 void NormalityConsistencyCheck(const Generator &rL, const EventSet &rOAlph, const Generator &rK) NormalityConsistencyCheck: Consistency check for normality input data. Definition: syn_supnorm.cpp:45 void SupConNormClosedUnchecked(const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rOAlph, Generator &rObserverGen, Generator &rSupCandGen) Supremal Normal Controllable Sublangauge (internal function) Definition: syn_supnorm.cpp:480 bool SupPrefixClosed(const Generator &rK, Generator &rResult) SupPrefixClosed: supremal closed sublanguage of K by cancelling all tranistions leading to a non-mark... Definition: syn_supnorm.cpp:419 void ConcatenateFullLanguage(Generator &rGen) ConcatenateFullLanguage: concatenate Sigma* to language marked by rGen. Definition: syn_supnorm.cpp:153 void ControlProblemConsistencyCheck(const GeneratorVector &rPlantGenVec, const EventSet &rConAlph, const GeneratorVector &rSpecGenVec) Compositional synthesis. Definition: syn_compsyn.cpp:1301 Supremal controllable sublanguage. Supremal normal sublanguage. libFAUDES 2.32b --- 2024.03.01 --- c++ api documentaion by doxygen |