cfl_bisimcta.cpp File Reference

Bisimulation relations (CTA) More...

#include "cfl_bisimcta.h"

Go to the source code of this file.

Classes
class	faudes::BisimulationCTA
	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. More...
struct	faudes::BisimulationCTA::State
class	faudes::AbstractBisimulationCTA
	The DelayedBisimulation class Derived from Bisimulation class. We implement the "two-pass change-tracking" algorithm from the cited paper. More...
class	faudes::TopoSort
	The TopoSort class perform a topological sort on states of a given automaton. if s1 is before s2 in the sort then there is no path from s2 to s1. The algorithm can be found in https://en.wikipedia.org/wiki/Topological_sorting under depth-first search, which is considered as first invented by R. Tarjan in 1976. More...
struct	faudes::TopoSort::State

Namespaces
	faudes
	libFAUDES resides within the namespace faudes.

Macros
#define	BISIM_VERB1(msg)
#define	BISIM_VERB0(msg)

Functions
bool	faudes::topoSort (const Generator &rGen, const EventSet &rEvs, std::list< Idx > &result)
	topoSort wrapper for topological sortation rEvs is the set of events which will be considered while sorting 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...
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...
void	faudes::ComputeDelayedBisimulationCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult)
void	faudes::ComputeBisimulationCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)
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::ComputeWeakBisimulation (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)
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...
void	faudes::ComputeDelayedBisimulationSatCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)
void	faudes::ComputeWeakBisimulationSatCTA (const Generator &rGen, const EventSet &rSilent, std::list< StateSet > &rResult, const std::vector< StateSet > &rPrePartition)

Detailed Description

Bisimulation relations (CTA)

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.cpp.

Macro Definition Documentation

BISIM_VERB0

#define BISIM_VERB0

(

msg

)

Value:

  { if((!faudes::ConsoleOut::G()->Mute()) && (faudes::ConsoleOut::G()->Verb() >=0 )) { \
      std::ostringstream cfl_line; cfl_line << msg << std::endl; faudes::ConsoleOut::G()->Write(cfl_line.str(),0,0,0);} }

Definition at line 47 of file cfl_bisimcta.cpp.

BISIM_VERB1

#define BISIM_VERB1

(

msg

)

Value:

  { if((!faudes::ConsoleOut::G()->Mute()) && (faudes::ConsoleOut::G()->Verb() >=1 )) { \
      std::ostringstream cfl_line; cfl_line << msg << std::endl; faudes::ConsoleOut::G()->Write(cfl_line.str(),0,0,0);} }

Definition at line 44 of file cfl_bisimcta.cpp.