cfl_bisimcta.h File Reference

Bisimulation relations. More...

#include "cfl_definitions.h"
#include "cfl_generator.h"
#include "cfl_nameset.h"
#include "cfl_indexset.h"
#include <vector>
#include <map>
#include <list>

Go to the source code of this file.

Namespaces
	faudes
	libFAUDES resides within the namespace faudes.

Functions
FAUDES_API void	faudes::FactorTauLoops (Generator &rGen, const Idx &rSilent)
	FactorTauLoops merge silent loop and then remove silent self loops. More...
void	faudes::ExtendTransRel (Generator &rGen, const EventSet &rSilent, const Idx &rFlag)
	ExtendTransRel perform transition saturation w.r.t. silent evs. Two different saturation modes are set depending on flag value. More...
void	faudes::InstallSelfloops (Generator &rGen, const EventSet &rEvs)
	InstallSelfloops install selfloops on all states of given event set. intended to install silent event selfloops for saturation. More...
void	faudes::ComputeBisimulationCTA (const Generator &rGen, std::list< StateSet > &rResult)
	ComputeBisimulationCTA basic bisimulation partition algorithm based on change-tracking algorithm. More...
FAUDES_API void	faudes::ComputeBisimulationCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult)
	ComputeBisimulationCTA bisimulation partition based on change-tracking algorithm and topo sort. More...
void	faudes::ComputeWeakBisimulationCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult)
	ComputeWeakBisimulationCTA weak bisimulation (aka observation eq) partition based on change-tracking algorithm and topo sort. More...
void	faudes::ComputeBisimulationCTA (const Generator &rGen, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)
	ComputeBisimulationCTA basic bisimulation partition algorithm under prepartition based on change-tracking algorithm. More...
FAUDES_API void	faudes::ComputeDelayedBisimulationCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)
	ComputeDelayedBisimulationCTA delayed bisimulation partition under prepartition based on change-tracking algorithm and topo sort. More...
FAUDES_API void	faudes::ComputeWeakBisimulationCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)
	ComputeWeakBisimulationCTA weak bisimulation (aka observation eq) partition under prepartition based on change-tracking algorithm and topo sort. More...
void	faudes::ComputeAbstractBisimulationSatCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const Idx &rFlag, const std::vector< StateSet > &rPrePartition)
	ComputeAbstractBisimulationSatCTA saturation and change-tracking based partition algorithm for either delayed or weak bisimulation. This function is intended to be invoked by ComputeDelayedBisimulation_Sat or ComputeWeakBisimulation_Sat, not for direct external usage. More...
void	faudes::ComputeDelayedBisimulationSatCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult)
	ComputeDelayedBisimulationSatCTA delayed bisimulation partition based on change-tracking algorithm and saturation. More...
void	faudes::ComputeWeakBisimulationSatCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult)
	ComputeWeakBisimulationSatCTA weak bisimulation (aka observation eq) partition based on change-tracking algorithm and saturation. More...
FAUDES_API void	faudes::ComputeComputeWeakBisimulationSatCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)
	ComputeComputeWeakBisimulationSatCTA weak bisimulation partition under prepartition based on change-tracking algorithm and saturation. More...

Detailed Description

Bisimulation relations.

Functions to compute bisimulation relations on dynamic systems (represented by non-deterministic finite automata).

More specifically, we we implement algorithms to obtain ordinary/delayed/weak bisimulations partitions based on change-tracking. In large, these implementations are expected to perform better than the classical variants found in cfl_bisimulation.h".

This code was originally developed by Yiheng Tang in the context of compositional verification in 2020/21.

Definition in file cfl_bisimcta.h.