omg_rabinctrl.cpp File Reference

#include "omg_rabinctrl.h"
#include "omg_rabinfnct.h"
#include "syn_include.h"

Go to the source code of this file.

Classes
class	faudes::RabinInvDynOperator
class	faudes::RabinInvDynTheta
class	faudes::RabinInvDynThetaTildeCore
class	faudes::RabinInvDynThetaTildeInner
class	faudes::RabinInvDynThetaTilde
class	faudes::RabinInvDynPReachCore
class	faudes::RabinInvDynPReach
class	faudes::RabinInvDynCtrlCore
class	faudes::RabinInvDynCtrlInner
class	faudes::RabinInvDynCtrl

Namespaces
	faudes

Functions
void	faudes::RabinCtrlPfx (const RabinAutomaton &rRAut, const EventSet &rSigmaCtrl, StateSet &rCtrlPfx)
void	faudes::RabinCtrlPfx (const RabinAutomaton &rRAut, const EventSet &rSigmaCtrl, TaIndexSet< EventSet > &rController)
void	faudes::RabinCtrlPfx (const RabinAutomaton &rRAut, const EventSet &rSigmaCtrl, Generator &rResGen)
void	faudes::SupRabinCon (const Generator &rBPlant, const EventSet &rCAlph, const RabinAutomaton &rRSpec, RabinAutomaton &rRes)
void	faudes::SupRabinCon (const System &rBPlant, const RabinAutomaton &rRSpec, RabinAutomaton &rRes)
void	faudes::RabinCtrl (const Generator &rBPlant, const EventSet &rCAlph, const RabinAutomaton &rRSpec, Generator &rRes)
void	faudes::RabinCtrl (const Generator &rBPlant, const EventSet &rCAlph, const Generator &rGLSpec, const RabinAutomaton &rRUSpec, Generator &rRes)
void	faudes::RabinCtrl (const System &rBPlant, const RabinAutomaton &rRSpec, Generator &rRes)
void	faudes::RabinCtrl (const System &rBPlant, const Generator &rBLSpec, const RabinAutomaton &rRUSpec, Generator &rRes)

Detailed Description

Controller synthesis for Rabin automata

Definition in file omg_rabinctrl.cpp.