diag_languagediagnosis.h File Reference

Functions to check a system's diagnosability with respect to a specification automaton and compute a language-diagnoser. More...

#include <vector>
#include "corefaudes.h"
#include "diag_generator.h"
#include "diag_eventdiagnosis.h"
#include "op_obserververification.h"
#include "diag_debug.h"

Go to the source code of this file.

Classes
struct	faudes::VerifierState

Namespaces
	faudes
	libFAUDES resides within the namespace faudes.

Enumerations
enum	faudes::VerifierStateLabel { faudes::NORMAL , faudes::CONFUSED , faudes::BLOCK }

Functions
void	faudes::ComputeGobs (const System &rGenMarkedNonSpecBehaviour, Diagnoser &rGobs)
	Compute G_o for a generator that marks the faulty behaviour of a plant. More...
FAUDES_API void	faudes::ComputeReachability (const System &rGen, const EventSet &rUnobsEvents, Idx State, std::map< Idx, std::multimap< Idx, DiagLabelSet > > &rReachabilityMap)
	Compute the reachability from a state of a generator that marks its faulty behaviour. More...
void	faudes::ComputeReachabilityRecursive (const System &rGen, const EventSet &rUnobsEvents, Idx State, StateSet done, std::map< Idx, std::multimap< Idx, DiagLabelSet > > &rReachabilityMap)
	Auxiliary function for ComputeReachability(const System&, const EventSet&, Idx State, std::map<Idx,std::multimap< Idx,DiagLabelSet> >&). More...
bool	faudes::IsLanguageDiagnosable (const System &rGen, const System &rSpec)
	Function definition for run-time interface. More...
bool	faudes::IsLanguageDiagnosable (const System &rGen, const System rSpec, std::string &rReportString)
	Test function to verify language-diagnosability. More...
bool	faudes::rec_ComputeLoopPreservingObserver (const System &rGen, const EventSet &rInitialHighAlph, EventSet &rHighAlph, const std::vector< Idx > &rDdffVector, Idx numberEvents, Idx currentNumberEvents, Idx currentLocation, EventSet chosenEvents)
	rec_ComputeLoopPreservingObserver(rGen, rInitialHighAlph, rHighAlph, rDdffVector, numberEvents, currentNumberEvents, currentLocation, hosenEvents) More...
Functions (diagnosability with respect to a specification)
FAUDES_API bool	faudes::IsLanguageDiagnosableX (const System &rGen, const System &rSpec, std::string &rReportString)
	Tests a system's diagnosability with respect to a given specification. More...
Functions (verification and computation of loop-preserving observers)
bool	faudes::IsLoopPreservingObserver (const System &rGen, const EventSet &rHighAlph)
	Verifies a loop-preserving observer. More...
void	faudes::LoopPreservingObserver (const System &rGen, const EventSet &rInitialHighAlph, EventSet &rHighAlph)
	Computes a loop-preserving observer with minimal state size of the abstraction. More...
Functions (diagnoser computation)
void	faudes::LanguageDiagnoser (const System &rGen, const System &rSpec, Diagnoser &rDiagGen)
	Compute a standard diagnoser from an input generator and a specification. More...

Detailed Description

Functions to check a system's diagnosability with respect to a specification automaton and compute a language-diagnoser.

Definition in file diag_languagediagnosis.h.