syn_compsyn.cpp File Reference

Compositional synthesis. More...

#include "syn_compsyn.h"
#include "syn_synthequiv.h"
#include "corefaudes.h"

Go to the source code of this file.

Classes
class	faudes::ComSyn
class	faudes::SmallSize

Namespaces
	faudes
	libFAUDES resides within the namespace faudes.

Functions
void	faudes::TransSpec (const GeneratorVector &rSpecGenVec, const EventSet &rGUncAlph, GeneratorVector &rResGenVec)
	translate specification into plant More...
void	faudes::ComputeWSOE (const Generator &rGenOrig, const EventSet &rConAlph, const EventSet &rLocAlph, std::map< Idx, Idx > &rMapStateToPartition, Generator &rResGen)
	weak synthesis obeservation equivalence [not implemented] More...
void	faudes::GlobalSelfloop (GeneratorVector &rGenVec)
	remove the events from the entire buffer which have only selfloop transitions More...
void	faudes::LocalSelfloop (Generator &rGen, EventSet &rLocAlph)
	remove the events from a generator which have only selfloop transitions More...
void	faudes::MakeDistinguisher (Generator &AbstGen, std::map< Idx, Idx > &rMapStateToPartition, Generator &OrigGen, std::map< Idx, std::vector< Idx > > &rMapOldToNew)
	make a distinguisher and a map for solving nondeterminism and rewrite abstracted automaton More...
void	faudes::Splitter (const std::map< Idx, std::vector< Idx > > &rMapOldToNew, EventSet &rConAlph, GeneratorVector &rGenVec, std::map< Idx, Idx > &rMapEventsToPlant, GeneratorVector &rDisGenVec, GeneratorVector &rSupGenVec)
	update the generators in synthesis-buffer and in supervisor with new events More...
void	faudes::SelectSubsystem_V1 (GeneratorVector &rGenVec, Generator &rResGen)
	heuristic: vorious approaches to select subsystem from synthesis-buffer then compose them and remove them from buffer. More...
void	faudes::SelectSubsystem_V2 (GeneratorVector &rGenVec, Generator &rResGen)
void	faudes::ComputeHSupConNB (const Generator &rOrigGen, const EventSet &rConAlph, const EventSet &rLocAlph, Generator &rHSupGen)
	halbway-synthesis More...
void	faudes::SingleTransSpec (const Generator &rSpecGen, const EventSet &rUncAlph, Generator &rResGen)
void	faudes::SplittGen (Generator &rGen, Idx parent, const std::vector< Idx > &kids)
	subfunction for Splitter: splitt the events in a generator More...
bool	faudes::BiggerMax (std::vector< GeneratorVector::Position > &rCandidate, GeneratorVector &rGenVec)
void	faudes::H_tocollect (StateSet &rBlockingstates, const TransSetX2EvX1 &rRtrel, const EventSet &rLouc, const EventSet &rShuc, TransSetX2EvX1 &rToredirect)
void	faudes::ControlProblemConsistencyCheck (const GeneratorVector &rPlantGenVec, const EventSet &rConAlph, const GeneratorVector &rSpecGenVec)
	Compositional synthesis. More...
void	faudes::CompositionalSynthesisUnchecked (const GeneratorVector &rPlantGenVec, const EventSet &rConAlph, const GeneratorVector &rSpecGenVec, std::map< Idx, Idx > &rMapEventsToPlant, GeneratorVector &rDisGenVec, GeneratorVector &rSupGenVec)
	Compositional synthesis. More...
void	faudes::CompositionalSynthesis (const GeneratorVector &rPlantGenVec, const EventSet &rConAlph, const GeneratorVector &rSpecGenVec, std::map< Idx, Idx > &rMapEventsToPlant, GeneratorVector &rDisGenVec, GeneratorVector &rSupGenVec)
	Compositional synthesis. More...

Detailed Description

Compositional synthesis.

Definition in file syn_compsyn.cpp.