omg_rabinctrl.h File Reference

#include "corefaudes.h"
#include "omg_rabinaut.h"

Go to the source code of this file.

Namespaces
	faudes

Functions
void	faudes::RabinCtrlPfx (const RabinAutomaton &rRAut, const EventSet &rSigmaCtrl, StateSet &rCtrlPfx)
void	faudes::RabinCtrlPfx (const RabinAutomaton &rRAut, const EventSet &rSigmaCtrl, Generator &rResGen)
void	faudes::RabinCtrlPfx (const RabinAutomaton &rRAut, const EventSet &rSigmaCtrl, TaIndexSet< EventSet > &rController)
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 System &rBPlant, 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 Generator &rBLSpec, const RabinAutomaton &rRUSpec, Generator &rRes)

Detailed Description

Controller synthesis for Rabin automata

Definition in file omg_rabinctrl.h.