Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
faudes::Candidate Class Reference

#include <pev_abstraction.h>

Public Member Functions

 Candidate (void)
 
 Candidate (Generator &goi)
 
 Candidate (Generator &goi, ProductCompositionMap map, std::pair< Candidate *, Candidate * > pair)
 
virtual ~Candidate ()
 
Generator GenRaw ()
 
Generator GenHidden ()
 
Generator GenMerged ()
 
std::map< Idx, Idx > MergeMap ()
 
std::set< Idx > FindConcreteStates (Idx abstract)
 
bool IsInMergedClass (Idx concrete, Idx abstract)
 
ProductCompositionMap ComposeMap ()
 
std::pair< Candidate *, Candidate * > DecomposedPair ()
 
EventSet Silentevs ()
 
void SetSilentevs (EventSet silentevs)
 
void ClearComposition ()
 
Idx Tau ()
 
void SetTau (Idx tau)
 
virtual void HidePrivateEvs (EventSet &silent)
 
void MergeEquivalenceClasses (Generator &rGen, TransSetX2EvX1 &rRevTrans, const std::list< StateSet > &rClasses, const EventSet &silent)
 
void ExtendedTransRel (const Generator &rGen, const EventSet &rSilentAlphabet, TransSet &rXTrans)
 
void IncomingTransSet (const Generator &rGen, const EventSet &silent, const Idx &state, std::set< std::pair< Idx, Idx >> &result)
 
void ActiveNonTauEvs (const Generator &rGen, const EventSet &silent, const Idx &state, EventSet &result)
 
void ObservationEquivalentQuotient (Generator &g, const EventSet &silent)
 
void ReverseObservationEquivalentQuotient (Generator &g, const EventSet &silent)
 
void WeakObservationEquivalentQuotient (Generator &g, const EventSet &silent)
 
void ActiveEventsANDEnabledContinuationRule (Generator &g, const EventSet &silent)
 
void RemoveTauSelfloops (Generator &g, const EventSet &silent)
 
virtual void MergeSilentLoops (Generator &g, const EventSet &silent)
 
void RemoveNonCoaccessibleOut (Generator &g)
 
void BlockingSilentEvent (Generator &g, const EventSet &silent)
 
void MergeNonCoaccessible (Generator &g)
 
void BlockingEvent (Generator &g, const EventSet &silent)
 
void OnlySilentIncoming (Generator &g, const EventSet &silent)
 
void OnlySilentOutgoing (Generator &g, const EventSet &silent)
 
virtual void ConflictEquivalentAbstraction (EventSet &silent)
 

Protected Member Functions

void DoAssign (Candidate cand)
 

Protected Attributes

Generator mGenRaw
 
Generator mGenHidden
 
Generator mGenMerged
 
std::map< Idx, Idx > mMergeMap
 
EventSet mSilentevs
 
Idx mtau = 0
 
ProductCompositionMap mComposeMap
 
std::pair< Candidate *, Candidate * > mDecomposedPair
 

Detailed Description

Definition at line 130 of file pev_abstraction.h.

Constructor & Destructor Documentation

◆ Candidate() [1/3]

faudes::Candidate::Candidate ( void  )
inline

Definition at line 132 of file pev_abstraction.h.

◆ Candidate() [2/3]

faudes::Candidate::Candidate ( Generator &  goi)

Definition at line 143 of file pev_verify.cpp.

◆ Candidate() [3/3]

faudes::Candidate::Candidate ( Generator &  goi,
ProductCompositionMap  map,
std::pair< Candidate *, Candidate * >  pair 
)

Definition at line 152 of file pev_verify.cpp.

◆ ~Candidate()

faudes::Candidate::~Candidate ( )
virtual

Definition at line 103 of file pev_verify.cpp.

Member Function Documentation

◆ ActiveEventsANDEnabledContinuationRule()

void faudes::Candidate::ActiveEventsANDEnabledContinuationRule ( Generator &  g,
const EventSet &  silent 
)

Definition at line 390 of file pev_abstraction.cpp.

◆ ActiveNonTauEvs()

void faudes::Candidate::ActiveNonTauEvs ( const Generator &  rGen,
const EventSet &  silent,
const Idx &  state,
EventSet &  result 
)

Definition at line 356 of file pev_abstraction.cpp.

◆ BlockingEvent()

void faudes::Candidate::BlockingEvent ( Generator &  g,
const EventSet &  silent 
)

Definition at line 595 of file pev_abstraction.cpp.

◆ BlockingSilentEvent()

void faudes::Candidate::BlockingSilentEvent ( Generator &  g,
const EventSet &  silent 
)

Definition at line 542 of file pev_abstraction.cpp.

◆ ClearComposition()

void faudes::Candidate::ClearComposition ( )
inline

Definition at line 146 of file pev_abstraction.h.

◆ ComposeMap()

ProductCompositionMap faudes::Candidate::ComposeMap ( )
inline

Definition at line 142 of file pev_abstraction.h.

◆ ConflictEquivalentAbstraction()

void faudes::Candidate::ConflictEquivalentAbstraction ( EventSet &  silent)
virtual

Reimplemented in faudes::PCandidate.

Definition at line 756 of file pev_abstraction.cpp.

◆ DecomposedPair()

std::pair<Candidate*,Candidate*> faudes::Candidate::DecomposedPair ( )
inline

Definition at line 143 of file pev_abstraction.h.

◆ DoAssign()

void faudes::Candidate::DoAssign ( Candidate  cand)
protected

Definition at line 116 of file pev_verify.cpp.

◆ ExtendedTransRel()

void faudes::Candidate::ExtendedTransRel ( const Generator &  rGen,
const EventSet &  rSilentAlphabet,
TransSet &  rXTrans 
)

Definition at line 133 of file pev_abstraction.cpp.

◆ FindConcreteStates()

std::set< Idx > faudes::Candidate::FindConcreteStates ( Idx  abstract)

Definition at line 164 of file pev_verify.cpp.

◆ GenHidden()

Generator faudes::Candidate::GenHidden ( )
inline

Definition at line 137 of file pev_abstraction.h.

◆ GenMerged()

Generator faudes::Candidate::GenMerged ( )
inline

Definition at line 138 of file pev_abstraction.h.

◆ GenRaw()

Generator faudes::Candidate::GenRaw ( )
inline

Definition at line 136 of file pev_abstraction.h.

◆ HidePrivateEvs()

void faudes::Candidate::HidePrivateEvs ( EventSet &  silent)
virtual

re-imp conflict-eq abstraction below

Reimplemented in faudes::PCandidate.

Definition at line 727 of file pev_abstraction.cpp.

◆ IncomingTransSet()

void faudes::Candidate::IncomingTransSet ( const Generator &  rGen,
const EventSet &  silent,
const Idx &  state,
std::set< std::pair< Idx, Idx >> &  result 
)

Definition at line 317 of file pev_abstraction.cpp.

◆ IsInMergedClass()

bool faudes::Candidate::IsInMergedClass ( Idx  concrete,
Idx  abstract 
)

Definition at line 175 of file pev_verify.cpp.

◆ MergeEquivalenceClasses()

void faudes::Candidate::MergeEquivalenceClasses ( Generator &  rGen,
TransSetX2EvX1 &  rRevTrans,
const std::list< StateSet > &  rClasses,
const EventSet &  silent 
)

Definition at line 41 of file pev_abstraction.cpp.

◆ MergeMap()

std::map<Idx,Idx> faudes::Candidate::MergeMap ( )
inline

Definition at line 139 of file pev_abstraction.h.

◆ MergeNonCoaccessible()

void faudes::Candidate::MergeNonCoaccessible ( Generator &  g)

Definition at line 573 of file pev_abstraction.cpp.

◆ MergeSilentLoops()

void faudes::Candidate::MergeSilentLoops ( Generator &  g,
const EventSet &  silent 
)
virtual

Reimplemented in faudes::PCandidate.

Definition at line 497 of file pev_abstraction.cpp.

◆ ObservationEquivalentQuotient()

void faudes::Candidate::ObservationEquivalentQuotient ( Generator &  g,
const EventSet &  silent 
)

Definition at line 182 of file pev_abstraction.cpp.

◆ OnlySilentIncoming()

void faudes::Candidate::OnlySilentIncoming ( Generator &  g,
const EventSet &  silent 
)

Definition at line 633 of file pev_abstraction.cpp.

◆ OnlySilentOutgoing()

void faudes::Candidate::OnlySilentOutgoing ( Generator &  g,
const EventSet &  silent 
)

Definition at line 692 of file pev_abstraction.cpp.

◆ RemoveNonCoaccessibleOut()

void faudes::Candidate::RemoveNonCoaccessibleOut ( Generator &  g)

Definition at line 528 of file pev_abstraction.cpp.

◆ RemoveTauSelfloops()

void faudes::Candidate::RemoveTauSelfloops ( Generator &  g,
const EventSet &  silent 
)

Definition at line 484 of file pev_abstraction.cpp.

◆ ReverseObservationEquivalentQuotient()

void faudes::Candidate::ReverseObservationEquivalentQuotient ( Generator &  g,
const EventSet &  silent 
)

Definition at line 220 of file pev_abstraction.cpp.

◆ SetSilentevs()

void faudes::Candidate::SetSilentevs ( EventSet  silentevs)
inline

Definition at line 145 of file pev_abstraction.h.

◆ SetTau()

void faudes::Candidate::SetTau ( Idx  tau)
inline

Definition at line 148 of file pev_abstraction.h.

◆ Silentevs()

EventSet faudes::Candidate::Silentevs ( )
inline

Definition at line 144 of file pev_abstraction.h.

◆ Tau()

Idx faudes::Candidate::Tau ( )
inline

Definition at line 147 of file pev_abstraction.h.

◆ WeakObservationEquivalentQuotient()

void faudes::Candidate::WeakObservationEquivalentQuotient ( Generator &  g,
const EventSet &  silent 
)

Definition at line 283 of file pev_abstraction.cpp.

Member Data Documentation

◆ mComposeMap

ProductCompositionMap faudes::Candidate::mComposeMap
protected

Definition at line 237 of file pev_abstraction.h.

◆ mDecomposedPair

std::pair<Candidate*, Candidate*> faudes::Candidate::mDecomposedPair
protected

Definition at line 238 of file pev_abstraction.h.

◆ mGenHidden

Generator faudes::Candidate::mGenHidden
protected

Definition at line 227 of file pev_abstraction.h.

◆ mGenMerged

Generator faudes::Candidate::mGenMerged
protected

Definition at line 228 of file pev_abstraction.h.

◆ mGenRaw

Generator faudes::Candidate::mGenRaw
protected

Definition at line 226 of file pev_abstraction.h.

◆ mMergeMap

std::map<Idx,Idx> faudes::Candidate::mMergeMap
protected

Definition at line 229 of file pev_abstraction.h.

◆ mSilentevs

EventSet faudes::Candidate::mSilentevs
protected

Definition at line 230 of file pev_abstraction.h.

◆ mtau

Idx faudes::Candidate::mtau = 0
protected

Definition at line 232 of file pev_abstraction.h.

The documentation for this class was generated from the following files:

libFAUDES 2.33c --- 2025.05.15 --- c++ api documentaion by doxygen

>>