|
|
||||||
|
pev_abstraction.cpp
Go to the documentation of this file.
75 // // if X2 of this transition is still in this class with a silent ev, skip -- we shall do selfloop removal extern
84 // // if X1 of this transition is still in this class with a silent ev, skip -- we shall do selfloop removal extern
136 void Candidate::ExtendedTransRel(const Generator& rGen, const EventSet& rSilentAlphabet, TransSet& rXTrans) {
261 std::list<StateSet> eqclasses_fine; // store result in new list, as some classes may be directly abandoned
397 // instead of directly set up std::set<TransSet>, we hope the set of pairs<Idx(source state), Idx(ev)>
685 // meaning that the deleted state has its merge map unchanged, but it will never be used because
687 // will not be utilized by line 12 of Algo 1, R. Malik and S. Ware 2018. Note we need the merge map
703 if (tit2==tit2_end) {sit++;continue;} // sit points to a deadend state (nonmarked state without outgoing trans)
742 if (msilentevs.Empty()){// in this case, only one 1 silent event is set to tau and no need to hide
908 // shape by set of preempting events only (TM2025: need this old version to compile/link example)
1044 void SaturateLowestPrio(const pGenerator& rPGen, const EventSet& rSilent, pGenerator& rResult){
1140 if (_mode==0 && !rSilent.Exists(tit1->Ev)) continue; // in mode 0, do not saturate non-sil trans
1153 && NonsilHigherThen(rPGen,rSilent,tit2->X1,tit1EvPrio)<=NonsilHigherThen(rPGen,rSilent,tit1->X1,tit1EvPrio)){
1169 && NonsilHigherThen(rPGen,rSilent,tit2->X1,tit1EvPrio)<=NonsilHigherThen(rPGen,rSilent,tit1->X1,tit1EvPrio)){
1189 // detect livelocks and store in rResult. rResult is a map of livelock->the SILENT EV whose priority describes the livelo
1191 void DetectLiveLocks(const pGenerator &rPGen, const EventSet &rSilent, std::map<StateSet, Idx>& rResult){
1339 void IncomingEquivalentClasses(const pGenerator& rPGen, const EventSet& rSilent, std::list<StateSet>& rResult){
1364 bool ok = IncomingTransSet(rPGen,closurefull,closurelowest,trans_full,trans_lowest,rSilent,*sit,rec_income);
1387 void AESCClasses(const pGenerator& rPGen, const EventSet& rSilent, std::list<StateSet>& rResult){
1390 std::map<StateSet, Idx> livelocks; // only need keys, values are livelock prios which are irrelevant
1431 NonsilHigherThen(rPGen,rSilent,*sit,tauprio).Size()+ NonsilHigherThen(rPGen,rSilent,cstate,tauprio).Size()==0){
1462 // figure out the highest possible k for =>_<k (with target not tau<k) transitions for each two states
1484 // in the following, highest's meaning is changed to "the highest k tit allows for successive transitions"
1488 Idx lowest = rPGen.LowestPriority(); // allowed lowest priority, changed if some tau is active on X2
1558 void OnlySilentIncoming(pGenerator& rPGen, const EventSet& rSilent, const StateSet& rLivelocks){
1592 if (rtit->X1 == tit3->X2 && rSilent.Exists(tit3->Ev)) continue; // avoid generating silent self loop
1610 void OnlySilentOutgoing(pGenerator& rPGen, const EventSet& rSilent, const StateSet& rLivelocks){
1621 if (tit2==tit2_end) {sit++;continue;} // sit points to a deadend state (nonmarked state without outgoing trans)
1636 if (rtit->X1 == tit2->X2 && rSilent.Exists( rtit->Ev)) continue; // avoid generating silent self loop
1697 StateSet sblock; // states with outgoing silent event with highest active priority and leads to block
1815 EventSet::Iterator eit = rSilent.Begin(); // NOTE: rSilent should be a subset of rPGen.Alphabet
1826 errstr << "Alphabet of '" << rPGen.Name() << "' inculdes reserved symbolic name " << silevname;
1847 RedundantSilentStep(rPGen,augsilent); // quick, may produce silent selfloop, guarantee well-formedness
1877 if (!rSilent.Exists(rTrans.Ev)) return false; // this is not a silent event at all (e.g. _OMEGA_)
1898 FairnessConstraints relevant_copy = relevant; // buffer a copy of relevant fairness constraints
1964 if (!IsHideable(rPGen,msilentevs+result,*tit)||result.Exists(tit->Ev)||unhideable.Exists(tit->Ev)){
2005 void MergeFairness(const pGenerator& rPGen1, const pGenerator& rPGen2, FairnessConstraints& rFairRes){
2017 // b) if rFairVec is empty we treat omega-termination as the acceptance condition (see below wraper)
2041 errstr << "Generator '"<<rGvec.At(git).Name() <<"' contains fairness event not in its alphabet";
2051 // if isSFC==1, set up merging events. Also check priority (disjunct is checked by SFC_Parallel)
2164 PCOMPVER_VERB1("Composing automata "<<pgenvec.at(imin).Name()<<" and "<<pgenvec.at(jmin).Name());
2178 newpgenvec.push_back(pgenvec.at(git)); // all other candidates are just copied to the next iteraion
2234 if (msilentevs.Empty() && mpsilentevs.Empty()){// in this case, only one 1 silent event is set to tau and no need to hide
2263 void PCandidate::ObservationEquivalenceQuotient_Preemptive(Generator &g, const EventSet &silent, const bool& flag){
void OnlySilentIncoming(Generator &g, const EventSet &silent) Definition: pev_abstraction.cpp:636 void BlockingSilentEvent(Generator &g, const EventSet &silent) Definition: pev_abstraction.cpp:545 virtual void HidePrivateEvs(EventSet &silent) Definition: pev_abstraction.cpp:730 void RemoveTauSelfloops(Generator &g, const EventSet &silent) Definition: pev_abstraction.cpp:487 void RemoveNonCoaccessibleOut(Generator &g) Definition: pev_abstraction.cpp:531 void ActiveNonTauEvs(const Generator &rGen, const EventSet &silent, const Idx &state, EventSet &result) Definition: pev_abstraction.cpp:359 void SetSilentevs(EventSet silentevs) Definition: pev_abstraction.h:145 void ActiveEventsANDEnabledContinuationRule(Generator &g, const EventSet &silent) Definition: pev_abstraction.cpp:393 void MergeEquivalenceClasses(Generator &rGen, TransSetX2EvX1 &rRevTrans, const std::list< StateSet > &rClasses, const EventSet &silent) Definition: pev_abstraction.cpp:44 virtual void MergeSilentLoops(Generator &g, const EventSet &silent) Definition: pev_abstraction.cpp:500 void OnlySilentOutgoing(Generator &g, const EventSet &silent) Definition: pev_abstraction.cpp:695 virtual void ConflictEquivalentAbstraction(EventSet &silent) Definition: pev_abstraction.cpp:759 void BlockingEvent(Generator &g, const EventSet &silent) Definition: pev_abstraction.cpp:598 void WeakObservationEquivalentQuotient(Generator &g, const EventSet &silent) Definition: pev_abstraction.cpp:286 void IncomingTransSet(const Generator &rGen, const EventSet &silent, const Idx &state, std::set< std::pair< Idx, Idx >> &result) Definition: pev_abstraction.cpp:320 void ReverseObservationEquivalentQuotient(Generator &g, const EventSet &silent) Definition: pev_abstraction.cpp:223 void ObservationEquivalentQuotient(Generator &g, const EventSet &silent) Definition: pev_abstraction.cpp:185 void ExtendedTransRel(const Generator &rGen, const EventSet &rSilentAlphabet, TransSet &rXTrans) Definition: pev_abstraction.cpp:136 void MergeNonCoaccessible(Generator &g) Definition: pev_abstraction.cpp:576 Definition: cfl_exception.h:118 Definition: cfl_indexset.h:78 Definition: cfl_nameset.h:70 virtual void InsertSet(const NameSet &rOtherSet) Definition: cfl_nameset.cpp:300 virtual void HidePrivateEvs(EventSet &silent) HidePrivateEvs replace all private events. Definition: pev_abstraction.cpp:2206 void SetPSilentevs(EventSet psilentevs) Definition: pev_abstraction.h:249 virtual void MergeSilentLoops(Generator &g, const EventSet &silent) Definition: pev_abstraction.cpp:2202 virtual void ConflictEquivalentAbstraction(EventSet &silent) Definition: pev_abstraction.cpp:2267 void ObservationEquivalenceQuotient_NonPreemptive(Generator &g, const EventSet &silent) Definition: pev_abstraction.cpp:2257 void ObservationEquivalenceQuotient_Preemptive(Generator &g, const EventSet &silent, const bool &flag) Definition: pev_abstraction.cpp:2263 Definition: cfl_baseset.h:394 std::vector< int >::size_type Position Definition: cfl_basevector.h:703 virtual Iterator Erase(const Iterator &vit) Definition: cfl_basevector.h:976 virtual const T & At(const Position &pos) const Definition: cfl_basevector.h:930 void RestrictEvents(const EventSet &rEventSet) Definition: cfl_transset.h:1689 TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator Definition: cfl_transset.h:273 void ReSort(TTransSet< OtherCmp > &res) const Definition: cfl_transset.h:1772 GlobalAttr * GlobalAttributep(void) Definition: cfl_agenerator.h:758 void EventAttribute(Idx index, const EventAttr &rAttr) Definition: cfl_agenerator.h:1287 EventAttr * EventAttributep(Idx index) Definition: cfl_agenerator.h:1312 const TaStateSet< StateAttr > & States(void) const Definition: cfl_agenerator.h:1363 const TaEventSet< EventAttr > & Alphabet(void) const Definition: cfl_agenerator.h:1358 bool SetTransition(Idx x1, Idx ev, Idx x2) Definition: cfl_agenerator.h:1197 void InjectTransRel(const TransSet &rNewtransrel) Definition: cfl_agenerator.h:1178 const ATransSet & TransRel(void) const Definition: cfl_agenerator.h:1368 void GlobalAttribute(const GlobalAttr &rAttr) Definition: cfl_agenerator.h:746 Definition: pev_priorities.h:197 Idx Priority(const std::string &rName) const Definition: pev_priorities.h:250 void InsPriority(const Idx idx, const Idx prio) Definition: pev_priorities.h:305 Definition: pev_pgenerator.h:139 FairnessConstraints Fairness(void) const Definition: pev_pgenerator.h:581 void HighestPriority(const Idx rPriority) Definition: pev_pgenerator.h:576 void Priorities(const TpEventSet< EventAttr > &rOtherSet) Definition: pev_pgenerator.h:537 Definition: cfl_transset.h:57 Definition: cfl_generator.h:213 StateSet::Iterator StatesBegin(void) const Definition: cfl_generator.cpp:1054 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 EventSet ActiveEventSet(Idx x1) const Definition: cfl_generator.cpp:1935 void DelEvents(const EventSet &rEvents) Definition: cfl_generator.cpp:1227 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 void InsEvents(const EventSet &events) Definition: cfl_generator.cpp:1207 EventSet::Iterator AlphabetBegin(void) const Definition: cfl_generator.cpp:1044 StateSet BlockingStates(void) const Definition: cfl_generator.cpp:2145 bool ExistsTransition(const std::string &rX1, const std::string &rEv, const std::string &rX2) const Definition: cfl_generator.cpp:1121 void InsStates(const StateSet &rStates) Definition: cfl_generator.cpp:1264 StateSet::Iterator MarkedStatesBegin(void) const Definition: cfl_generator.cpp:1157 StateSet::Iterator StatesEnd(void) const Definition: cfl_generator.cpp:1059 void DelStates(const StateSet &rDelStates) Definition: cfl_generator.cpp:1378 TransSet::Iterator TransRelEnd(void) const Definition: cfl_generator.cpp:1069 StateSet::Iterator MarkedStatesEnd(void) const Definition: cfl_generator.cpp:1162 void InjectTransRel(const TransSet &rNewtransrel) Definition: cfl_generator.cpp:1585 StateSet::Iterator InitStatesEnd(void) const Definition: cfl_generator.cpp:1152 void SetDefaultStateNames(void) Definition: cfl_generator.cpp:1012 std::string EventName(Idx index) const Definition: cfl_generator.cpp:836 EventSet::Iterator AlphabetEnd(void) const Definition: cfl_generator.cpp:1049 StateSet CoaccessibleSet(void) const Definition: cfl_generator.cpp:2051 bool ExistsInitState(Idx index) const Definition: cfl_generator.cpp:1793 bool ExistsMarkedState(Idx index) const Definition: cfl_generator.cpp:1803 void InjectAlphabet(const EventSet &rNewalphabet) Definition: cfl_generator.cpp:1167 virtual void InsertSet(const TBaseSet &rOtherSet) Definition: cfl_baseset.h:2052 void ComputeBisimulation(const Generator &rGenOrig, map< Idx, Idx > &rMapStateToPartition) Definition: cfl_bisimulation.cpp:1272 bool ComputeScc(const Generator &rGen, const SccFilter &rFilter, std::list< StateSet > &rSccList, StateSet &rRoots) Definition: cfl_graphfncts.cpp:347 void ShapePriorities(vGenerator &rGen, const EventPriorities &rPrios) Definition: pev_abstraction.cpp:893 void ShapePreemption(Generator &rGen, const EventSet &pevs) Definition: pev_abstraction.cpp:909 bool IsPFNonblocking(const GeneratorVector &rGvec, const EventPriorities &rPrios, const std::vector< FairnessConstraints > &rFairVec) Definition: pev_abstraction.cpp:2018 bool IsPNonblocking(const GeneratorVector &rGvec, const EventPriorities &rPrios) Definition: pev_abstraction.cpp:2189 Definition: cfl_agenerator.h:43 void BlockingSilentEvent(Generator &g, const EventSet &silent) Definition: cfl_conflequiv.cpp:386 std::map< std::pair< Idx, Idx >, EventSet > IncTransSet Definition: pev_abstraction.cpp:1258 void IncomingTransSet(const Generator &rGen, const TransSetX2EvX1 &rRTrans, const EventSet &silent, const Idx &state, SetX1Ev &result) Definition: cfl_conflequiv.cpp:152 EventSet NonsilHigherThen(const pGenerator &rPGen, const EventSet &rSilent, const Idx &rState, const Idx &rK) Definition: pev_abstraction.cpp:947 void UParallel_MergeFairness(const pGenerator &rPGen1, const pGenerator &rPGen2, const Generator &rGen12, const EventSet &rMerge, FairnessConstraints &rFairRes) Definition: pev_sparallel.cpp:331 void AppendOmegaTermination(Generator &rGen) Definition: cfl_conflequiv.cpp:52 void OnlySilentIncoming(Generator &g, const EventSet &silent) Definition: cfl_conflequiv.cpp:441 StateSet StronglyCoaccessibleSet(const pGenerator &rPGen) Definition: pev_abstraction.cpp:1655 void RemoveNonCoaccessibleOut(Generator &g) Definition: cfl_conflequiv.cpp:372 bool IsHideable(const pGenerator &rPGen, const EventSet &rSilent, const Transition &rTrans) Definition: pev_abstraction.cpp:1873 void MergeEquivalenceClasses(Generator &rGen, TransSetX2EvX1 &rRevTrans, const std::list< StateSet > &rClasses) Definition: cfl_conflequiv.cpp:74 void OnlySilentOutgoing(Generator &g, const EventSet &silent) Definition: cfl_conflequiv.cpp:496 Idx SilentEvAtPrio(const pGenerator &rPGen, const EventSet &rSilent, const Idx &rK) Definition: pev_abstraction.cpp:967 bool IsNonblocking(const GeneratorVector &rGvec) Definition: cfl_conflequiv.cpp:705 std::map< SetX1Ev, StateSet > IncomingEquivalentClasses(const Generator &rGen, const EventSet &silent) Definition: cfl_conflequiv.cpp:222 void SaturatePWB(const pGenerator &rPGen, const EventSet &rSilent, pGenerator &rResult) Definition: pev_abstraction.cpp:1453 void PrintEqclasses(const std::list< StateSet > &rEqclasses) Definition: pev_abstraction.cpp:804 void ShapeUpsilon(vGenerator &rGen, const EventPriorities &rPrios, const EventSet &rUpsilon) Definition: pev_abstraction.cpp:855 void PrintEventTable(const pGenerator &rPGen) Definition: pev_abstraction.cpp:797 EventSet HidePrivateEvs(pGenerator &rPGen, EventSet &rPrivate, EventPriorities &rPrios, Idx &rTau, const EventSet *pUnHideable=nullptr) Definition: pev_abstraction.cpp:1930 void MergeAESC(pGenerator &rPGen, const EventSet &rSilent) Definition: pev_abstraction.cpp:1444 void SUParallel(const pGenerator &rPGen1, const pGenerator &rPGen2, std::map< std::pair< Idx, Idx >, Idx > &rCompositionMap, EventSet &rMerge, const EventSet &rPrivate, EventPriorities &rPrios, pGenerator &rPRes) Definition: pev_sparallel.cpp:43 void PConflictPreservingAbstraction(pGenerator &rPGen, const EventSet &rSilent) Definition: pev_abstraction.cpp:1806 void RemoveRedSilentSelfloops(pGenerator &rPGen, const EventSet &rSilent) Definition: pev_abstraction.cpp:928 void ComputeBisimulationCTA(const Generator &rGen, std::list< StateSet > &rResult) ComputeBisimulationCTA basic bisimulation partition algorithm based on change-tracking algorithm. Definition: cfl_bisimcta.cpp:924 void MergePWB(pGenerator &rPGen, const EventSet &rSilent) Definition: pev_abstraction.cpp:1510 void AESCClasses(const pGenerator &rPGen, const EventSet &rSilent, std::list< StateSet > &rResult) Definition: pev_abstraction.cpp:1387 bool IsStronglyNonblocking(const pGenerator &rPGen) Definition: pev_abstraction.cpp:1979 void BlockingEvent(pGenerator &rPGen, const EventSet &rSilent) Definition: pev_abstraction.cpp:1765 void RedundantSilentStep(pGenerator &rPGen, const EventSet &rSilent) Definition: pev_abstraction.cpp:1521 void DetectLiveLocks(const pGenerator &rPGen, const EventSet &rSilent, std::map< StateSet, Idx > &rResult) Definition: pev_abstraction.cpp:1191 void SaturateLowestPrio(const pGenerator &rPGen, const EventSet &rSilent, pGenerator &rResult) Definition: pev_abstraction.cpp:1044 void MergeFairness(const pGenerator &rPGen1, const pGenerator &rPGen2, FairnessConstraints &rFairRes) Definition: pev_abstraction.cpp:2005 void MergeNonCoaccessible(Generator &g) Definition: cfl_conflequiv.cpp:417 void SaturatePDelayed(const pGenerator &rPGen, const EventSet &rSilent, const bool &_mode, pGenerator &rResult) Definition: pev_abstraction.cpp:1106 libFAUDES 2.33h --- 2025.06.18 --- c++ api documentaion by doxygen |