omg_rabinctrlpartialobs.h File Reference

#include "libfaudes.h"
#include "omg_rabinaut.h"
#include "omg_pseudodet.h"

Go to the source code of this file.

Namespaces
	faudes

Functions
void	faudes::RabinCtrlPartialObs (const System &rPlant, const RabinAutomaton &rSpec, RabinAutomaton &rSupervisor)
	Rabin control synthesis under partial observation (System interface) More...
void	faudes::RabinCtrlPartialObs (const RabinAutomaton &rPlant, const EventSet &rControllableEvents, const EventSet &rObservableEvents, const RabinAutomaton &rSpec, RabinAutomaton &rSupervisor)
	Rabin control synthesis under partial observation (with explicit event sets) More...
void	faudes::RabinCtrlPartialObsConsistencyCheck (const RabinAutomaton &rPlant, const RabinAutomaton &rSpec, const EventSet &rControllableEvents, const EventSet &rObservableEvents)
	Check consistency of control problem setup. More...
void	faudes::ExtractEventAttributes (const System &rSys, EventSet &rControllableEvents, EventSet &rObservableEvents)
	Extract controllable and observable events from System attributes. More...
void	faudes::ControlAut (const RabinAutomaton &rsDRA, const TaIndexSet< EventSet > &rController, Generator &rRes)
	Apply controller to filter transitions and create Buchi automaton. More...
void	faudes::EpsObservation (const RabinAutomaton &rGen, RabinAutomaton &rRes)
	Epsilon observation for Rabin automata. More...
void	faudes::EpsObservation (const System &rGen, System &rRes)
	Replace unobservable events with epsilon events for System types. More...
Generator	faudes::CreateMutedAutomaton (const Generator &rOriginal, const StateSet &rStatesToMute)
	Create muted automaton by removing specified states and their transitions. More...
bool	faudes::RabinLanguageInclusion (const System &rGenL, const RabinAutomaton &rRabK)
	Verify language inclusion for Rabin automata. More...

Detailed Description

Rabin control synthesis under partial observation

This module implements high-level API functions for supervisory control synthesis of Rabin automata under partial observation constraints.

Definition in file omg_rabinctrlpartialobs.h.