faudes::AbstractBisimulationCTA Class Reference

Detailed Description

The DelayedBisimulation class Derived from Bisimulation class. We implement the "two-pass change-tracking" algorithm from the cited paper.

Definition at line 197 of file cfl_bisimcta.cpp.

Public Member Functions
	AbstractBisimulationCTA (const Generator &rGen, const Idx &rSilent, const Idx &rTaskFlag, const std::vector< StateSet > &rPrePartition)
virtual void	ComputePartition (std::list< StateSet > &rResult)
	BisimulationPartition wrapper.

Private Member Functions
virtual void	EncodeData (void)
	EncodeData basic preparation for bisimulation NOTE: this function is virtual since derived classes, in the context of abstraction, have different steps.
void	MarkTauStarAffected (std::vector< bool > &rAffected, const Idx &rState)
	MarkTauAffected perform a recursive Depth-First-Search to mark all tau* predecessors as affected based on given state index rState. NOTE: rState is also a tau* predecessor of itself, thus also affected NOTE: as tau-loop-free is guaranteed, no need to use visited list to avoid duplet NOTE: in most cases, argument rAffected directly takes mAffected. The only exception is that in ComputeChangedObservedAfters, we need to buffer an intermediate affected-vector.
void	ComputeAbstractBisimulation ()
	ComputeDelayedBisimulation perform the overall iteration based on different task flag value, see mTaskFlag.
void	ComputeChangedDelayedAfters (void)
	ComputeChangedDelayedAfters see Fig. 10 of cited paper.
void	ComputeChangedObservedAfters (void)
	ComputeChangedObservedAfters see Fig. 12 of cited paper.
Private Member Functions inherited from faudes::BisimulationCTA
	BisimulationCTA (const Generator &rGen, const std::vector< StateSet > &rPrePartition)
virtual	~BisimulationCTA ()=default
void	FirstStepApproximation (void)
	FirstStepApproximation (see Fig. 2 (b) in cited paper) Prepartition states according to their active events. If a prepartition already exists, this function will refine the prepartition.
void	RefineChanged (void)
	RefineChanged refine equivalence classes contained affected nodes in the last iteration (see Fig. 5 in cited paper)
void	GenerateResult (std::list< StateSet > &rResult)
	GenerateResult generate partition result w.r.t. original state indices (without trivial classes)
bool	order_evs_c (const Idx &state1, const Idx &state2) const

Private Attributes
const Idx	mTau
	tau persist index of original silent event
const Idx	mTaskFlag
	mTaskFlag flag for task: mTaskFlag == 1: delayed bisimulation mTaskFlag == 2: weak bisimulation
Private Attributes inherited from faudes::BisimulationCTA
std::vector< State >	mStates
std::vector< Idx >	mEvents
const Generator *	mGen
const std::vector< StateSet >	mPrePartition
std::vector< bool >	mAffected
std::vector< bool >	mChanged
Idx	mCmax
Idx	mStateSize
Idx	mAlphSize
std::vector< Idx >	mPartition

Constructor & Destructor Documentation

AbstractBisimulationCTA()

faudes::AbstractBisimulationCTA::AbstractBisimulationCTA ( const Generator &  rGen, const Idx &  rSilent, const Idx &  rTaskFlag, const std::vector< StateSet > &  rPrePartition  )

inline

Definition at line 199 of file cfl_bisimcta.cpp.

Member Function Documentation

ComputeAbstractBisimulation()

void faudes::AbstractBisimulationCTA::ComputeAbstractBisimulation ( )

private

ComputeDelayedBisimulation perform the overall iteration based on different task flag value, see mTaskFlag.

Definition at line 914 of file cfl_bisimcta.cpp.

ComputeChangedDelayedAfters()

void faudes::AbstractBisimulationCTA::ComputeChangedDelayedAfters ( void  )

private

ComputeChangedDelayedAfters see Fig. 10 of cited paper.

Definition at line 810 of file cfl_bisimcta.cpp.

ComputeChangedObservedAfters()

void faudes::AbstractBisimulationCTA::ComputeChangedObservedAfters ( void  )

private

ComputeChangedObservedAfters see Fig. 12 of cited paper.

Definition at line 855 of file cfl_bisimcta.cpp.

ComputePartition()

void faudes::AbstractBisimulationCTA::ComputePartition ( std::list< StateSet > &  rResult )

virtual

BisimulationPartition wrapper.

Reimplemented from faudes::BisimulationCTA.

Definition at line 933 of file cfl_bisimcta.cpp.

EncodeData()

void faudes::AbstractBisimulationCTA::EncodeData ( void  )

privatevirtual

EncodeData basic preparation for bisimulation NOTE: this function is virtual since derived classes, in the context of abstraction, have different steps.

Reimplemented from faudes::BisimulationCTA.

Definition at line 689 of file cfl_bisimcta.cpp.

MarkTauStarAffected()

void faudes::AbstractBisimulationCTA::MarkTauStarAffected ( std::vector< bool > &  rAffected, const Idx &  rState  )

private

MarkTauAffected perform a recursive Depth-First-Search to mark all tau* predecessors as affected based on given state index rState. NOTE: rState is also a tau* predecessor of itself, thus also affected NOTE: as tau-loop-free is guaranteed, no need to use visited list to avoid duplet NOTE: in most cases, argument rAffected directly takes mAffected. The only exception is that in ComputeChangedObservedAfters, we need to buffer an intermediate affected-vector.

Definition at line 800 of file cfl_bisimcta.cpp.

Member Data Documentation

mTaskFlag

const Idx faudes::AbstractBisimulationCTA::mTaskFlag

private

mTaskFlag flag for task: mTaskFlag == 1: delayed bisimulation mTaskFlag == 2: weak bisimulation

Definition at line 217 of file cfl_bisimcta.cpp.

mTau

const Idx faudes::AbstractBisimulationCTA::mTau

private

tau persist index of original silent event

Definition at line 209 of file cfl_bisimcta.cpp.

---

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

• cfl_bisimcta.cpp