op_obserververification.h File Reference

#include "corefaudes.h"
#include "op_debug.h"
#include "op_observercomputation.h"
#include <map>
#include <vector>
#include <stack>

Go to the source code of this file.

Namespaces
	faudes

Functions
bool	faudes::IsObs (const Generator &rLowGen, const EventSet &rHighAlph)
bool	faudes::IsMSA (const Generator &rLowGen, const EventSet &rHighAlph)
bool	faudes::IsOCC (const System &rLowGen, const EventSet &rHighAlph)
bool	faudes::IsOCC (const Generator &rLowGen, const EventSet &rControllableEvents, const EventSet &rHighAlph)
bool	faudes::backwardVerificationOCC (const Generator &rLowGen, const EventSet &rControllableEvents, const EventSet &rHighAlph, Idx currentState)
bool	faudes::IsLCC (const System &rLowGen, const EventSet &rHighAlph)
bool	faudes::IsLCC (const Generator &rLowGen, const EventSet &rControllableEvents, const EventSet &rHighAlph)
FAUDES_API void	faudes::backwardVerificationLCC (const TransSetX2EvX1 &rTransSetX2EvX1, const EventSet &rControllableEvents, const EventSet &rHighAlph, Idx exitState, Idx currentState, bool controllablePath, std::map< Idx, bool > &rLocalStatesMap, StateSet &rDoneStates)

Detailed Description

Methods to verify the obsrver condition for natural projections. The observer condition is, e.g., defined in K. C. Wong and W. M. Wonham, “Hierarchical control of discrete-event systems,” Discrete Event Dynamic Systems: Theory and Applications, 1996. In addition, methods to verify output control consistency (OCC) and local control consistency (LCC) are provided. See for example K. Schmidt and C. Breindl, "On Maximal Permissiveness of Hierarchical and Modular Supervisory Control Approaches for Discrete Event Systems," Workshop on Discrete Event Systems, 2008.

Definition in file op_obserververification.h.