faudes::BisimulationCTA Class Reference

Detailed Description

The Bisimulation class The following class implements a basic normal bisimulation partition algorithms and derives a class for partitioning w.r.t. delayed bisimulation and weak bisimulation . All these algorithms are introduced in "Computing Maximal Weak and Other Bisimulations" from Alexandre Boulgakov et. al. (2016). The utilised normal bisimulation algorithm originates from the "change tracking algorithm" from Stefan Blom and Simona Orzan (see ref. of cited paper). Besides, the current paper uses topological sorted states to avoid computing saturated transitions explicitly when computing delayed and weak bisimulation.

IMPORTANT NOTE: both algorithms for delayed and weak bisimulation requires tau-loop free automaton. This shall be done extern beforehand by using e.g. FactorTauLoops(Generator &rGen, const Idx &rSilent).

Definition at line 74 of file cfl_bisimcta.cpp.

Classes
struct	State

Public Member Functions
	BisimulationCTA (const Generator &rGen, const std::vector< StateSet > &rPrePartition)
virtual	~BisimulationCTA ()=default
virtual void	ComputePartition (std::list< StateSet > &rResult)
	BisimulationPartition wrapper. More...

Protected Member Functions
virtual void	EncodeData (void)
	EncodeData encode source generator into vector-form data structures to accelerate the iteration. More...
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. More...
void	RefineChanged (void)
	RefineChanged refine equivalence classes contained affected nodes in the last iteration (see Fig. 5 in cited paper) More...
void	GenerateResult (std::list< StateSet > &rResult)
	GenerateResult generate partition result w.r.t. original state indices (without trivial classes) More...

Protected Attributes
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

Private Member Functions
void	ComputeBisimulation (void)
	ComputeBisimulation perform the overall iteration. More...
void	ComputeChangedAfters (void)
	ComputeChangedAfters Compute changed afters of each affected state. (see Fig 5. in cited paper) Affected states are those having some successors that have changed class (namely c_value) in the last iteration NOTE: this function is made private in that derived classes compute cafters w.r.t. silent event and these are accomplished by ComputeChangedDelayedAfters and ComputeChangedObservedAfters, respectively. More...

Constructor & Destructor Documentation

BisimulationCTA()

faudes::BisimulationCTA::BisimulationCTA ( const Generator &  rGen, const std::vector< StateSet > &  rPrePartition  )

inline

Definition at line 76 of file cfl_bisimcta.cpp.

~BisimulationCTA()

virtual faudes::BisimulationCTA::~BisimulationCTA ( )

virtualdefault

Member Function Documentation

ComputeBisimulation()

void faudes::BisimulationCTA::ComputeBisimulation ( void  )

private

ComputeBisimulation perform the overall iteration.

Definition at line 631 of file cfl_bisimcta.cpp.

ComputeChangedAfters()

void faudes::BisimulationCTA::ComputeChangedAfters ( void  )

private

ComputeChangedAfters Compute changed afters of each affected state. (see Fig 5. in cited paper) Affected states are those having some successors that have changed class (namely c_value) in the last iteration NOTE: this function is made private in that derived classes compute cafters w.r.t. silent event and these are accomplished by ComputeChangedDelayedAfters and ComputeChangedObservedAfters, respectively.

Definition at line 525 of file cfl_bisimcta.cpp.

ComputePartition()

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

virtual

BisimulationPartition wrapper.

Reimplemented in faudes::AbstractBisimulationCTA.

Definition at line 661 of file cfl_bisimcta.cpp.

EncodeData()

void faudes::BisimulationCTA::EncodeData ( void  )

protectedvirtual

EncodeData encode source generator into vector-form data structures to accelerate the iteration.

NOTE: this function is virtual since derived classes, in the context of abstraction, have different steps

Reimplemented in faudes::AbstractBisimulationCTA.

Definition at line 432 of file cfl_bisimcta.cpp.

FirstStepApproximation()

void faudes::BisimulationCTA::FirstStepApproximation ( void  )

protected

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.

NOTE: this function is also utilised by delayed- and weak-bisimulation since in both cases, State.evs neglect tau (as tau is always active)

Definition at line 502 of file cfl_bisimcta.cpp.

GenerateResult()

void faudes::BisimulationCTA::GenerateResult ( std::list< StateSet > &  rResult )

protected

GenerateResult generate partition result w.r.t. original state indices (without trivial classes)

Parameters

rResult

partition w.r.t. original state indices without trivial classes

Definition at line 644 of file cfl_bisimcta.cpp.

RefineChanged()

void faudes::BisimulationCTA::RefineChanged ( void  )

protected

RefineChanged refine equivalence classes contained affected nodes in the last iteration (see Fig. 5 in cited paper)

Definition at line 551 of file cfl_bisimcta.cpp.

Member Data Documentation

mAffected

std::vector<bool> faudes::BisimulationCTA::mAffected

protected

persisted data structures, see cited paper.

Definition at line 144 of file cfl_bisimcta.cpp.

mAlphSize

Idx faudes::BisimulationCTA::mAlphSize

protected

Definition at line 150 of file cfl_bisimcta.cpp.

mChanged

std::vector<bool> faudes::BisimulationCTA::mChanged

protected

Definition at line 145 of file cfl_bisimcta.cpp.

mCmax

Idx faudes::BisimulationCTA::mCmax

protected

Definition at line 146 of file cfl_bisimcta.cpp.

mEvents

std::vector<Idx> faudes::BisimulationCTA::mEvents

protected

Definition at line 101 of file cfl_bisimcta.cpp.

mGen

const Generator* faudes::BisimulationCTA::mGen

protected

keep the original generator

Definition at line 138 of file cfl_bisimcta.cpp.

mPartition

std::vector<Idx> faudes::BisimulationCTA::mPartition

protected

the current (and also final) partition. Partition is represented by states sorted by c_value. Access mStates for c_value to get the exact partition.

Definition at line 155 of file cfl_bisimcta.cpp.

mPrePartition

const std::vector<StateSet> faudes::BisimulationCTA::mPrePartition

protected

state prepartition with original state idx (the same as state label as in cited paper). Empty for trivial prepartition.

Definition at line 141 of file cfl_bisimcta.cpp.

mStates

std::vector<State> faudes::BisimulationCTA::mStates

protected

Definition at line 100 of file cfl_bisimcta.cpp.

mStateSize

Idx faudes::BisimulationCTA::mStateSize

protected

constant parameters for encoding

Definition at line 149 of file cfl_bisimcta.cpp.

---

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

• cfl_bisimcta.cpp