|
| void | faudes::PrintEventTable (const pGenerator &rPGen) |
| |
| void | faudes::PrintEqclasses (const std::list< StateSet > &rEqclasses) |
| |
| void | faudes::AppendOmegaTermination (pGenerator &rPGen, EventPriorities &rPrios) |
| |
| void | faudes::WritePrio (const pGenerator &rPGen) |
| |
| void | faudes::ShapeUpsilon (vGenerator &rGen, const EventPriorities &rPrios, const EventSet &rUpsilon) |
| |
| void | faudes::ShapeUpsilon (pGenerator &rPGen, const EventSet &rUpsilon) |
| |
| void | faudes::ShapePriorities (vGenerator &rGen, const EventPriorities &rPrios) |
| |
| void | faudes::ShapePriorities (pGenerator &rPGen) |
| |
| void | faudes::ShapePreemption (Generator &rGen, const EventSet &pevs) |
| |
| void | faudes::RemoveRedSilentSelfloops (pGenerator &rPGen, const EventSet &rSilent) |
| |
| EventSet | faudes::NonsilHigherThen (const pGenerator &rPGen, const EventSet &rSilent, const Idx &rState, const Idx &rK) |
| |
| Idx | faudes::SilentEvAtPrio (const pGenerator &rPGen, const EventSet &rSilent, const Idx &rK) |
| |
| void | faudes::MergeEquivalenceClasses (pGenerator &rPGen, const EventSet &rSilent, const std::map< StateSet, Idx > &rLivelocks, const std::list< StateSet > &rClasses) |
| |
| void | faudes::SaturateLowestPrio (const pGenerator &rPGen, const EventSet &rSilent, pGenerator &rResult) |
| |
| void | faudes::SaturatePDelayed (const pGenerator &rPGen, const EventSet &rSilent, const bool &_mode, pGenerator &rResult) |
| |
| void | faudes::DetectLiveLocks (const pGenerator &rPGen, const EventSet &rSilent, std::map< StateSet, Idx > &rResult) |
| |
| bool | faudes::IncomingTransSet (const pGenerator &rPGen, const pGenerator &rClosureFull, const pGenerator &rClosureLowest, const TransSetX2EvX1 &rtrans_full, const TransSetX2EvX1 &rtrans_lowest, const EventSet &rSilent, const Idx &rState, IncTransSet &rResult) |
| |
| void | faudes::IncomingEquivalentClasses (const pGenerator &rPGen, const EventSet &rSilent, std::list< StateSet > &rResult) |
| |
| void | faudes::AESCClasses (const pGenerator &rPGen, const EventSet &rSilent, std::list< StateSet > &rResult) |
| |
| void | faudes::MergeAESC (pGenerator &rPGen, const EventSet &rSilent) |
| |
| void | faudes::SaturatePWB (const pGenerator &rPGen, const EventSet &rSilent, pGenerator &rResult) |
| |
| void | faudes::MergePWB (pGenerator &rPGen, const EventSet &rSilent) |
| |
| void | faudes::RedundantSilentStep (pGenerator &rPGen, const EventSet &rSilent) |
| |
| void | faudes::OnlySilentIncoming (pGenerator &rPGen, const EventSet &rSilent, const StateSet &rLivelocks) |
| |
| void | faudes::OnlySilentOutgoing (pGenerator &rPGen, const EventSet &rSilent, const StateSet &rLivelocks) |
| |
| StateSet | faudes::StronglyCoaccessibleSet (const pGenerator &rPGen) |
| |
| void | faudes::RemoveNonCoaccessibleOut (pGenerator &rPGen) |
| |
| void | faudes::BlockingSilentEvent (pGenerator &rPGen, const EventSet &rSilent) |
| |
| void | faudes::MergeNonCoaccessible (pGenerator &rPGen) |
| |
| void | faudes::BlockingEvent (pGenerator &rPGen, const EventSet &rSilent) |
| |
| void | faudes::PConflictPreservingAbstraction (pGenerator &rPGen, const EventSet &rSilent) |
| |
| bool | faudes::IsHideable (const pGenerator &rPGen, const EventSet &rSilent, const Transition &rTrans) |
| |
| EventSet | faudes::HidePrivateEvs (pGenerator &rPGen, EventSet &rPrivate, EventPriorities &rPrios, Idx &rTau, const EventSet *pUnHideable=nullptr) |
| |
| bool | faudes::IsStronglyNonblocking (const pGenerator &rPGen) |
| |
| void | faudes::MergeFairness (const pGenerator &rPGen1, const pGenerator &rPGen2, FairnessConstraints &rFairRes) |
| |
| bool | faudes::IsPFNonblocking (const GeneratorVector &rGvec, const EventPriorities &rPrios, const std::vector< FairnessConstraints > &rFairVec) |
| |
| bool | faudes::IsPNonblocking (const GeneratorVector &rGvec, const EventPriorities &rPrios) |
| |
Conflict preserving abstractions
Definition in file pev_abstraction.cpp.