Detailed Description

This plug-in implements functions that are related to controllability and normality, as originally proposed by W.M. Wonham et al in the 1980s and selected extensions thereof. Examples are provided in the user reference, section Synthesis.

License

This plug-in is distributed with libFAUDES and under the terms of the LGPL.

Copyright (c) 2006, Bernd Opitz
Copyright (c) 2009, Thomas Moor, Sebastian Perk, Klaus Schmidt.
Copyright (c) 2010 - 2014, Thomas Moor.

Functions
void	faudes::CompositionalSynthesis (const GeneratorVector &rPlantGenVec, const EventSet &rConAlph, const GeneratorVector &rSpecGenVec, std::map< Idx, Idx > &rMapEventsToPlant, GeneratorVector &rDisGenVec, GeneratorVector &rSupGenVec)
	Compositional synthesis. More...

bool	faudes::IsRelativelyMarked (const Generator &rGenPlant, const Generator &rGenCand)
	Test for relative marking. More...

bool	faudes::IsRelativelyPrefixClosed (const Generator &rGenPlant, const Generator &rGenCand)
	Test for relative prefix-closedness. More...

void	faudes::SupRelativelyPrefixClosed (const Generator &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
	Supremal Relatively Closed Sublanguage. More...

bool	faudes::IsRelativelyOmegaMarked (const Generator &rGenPlant, const Generator &rGenCand)
	Test for relative marking, omega langauges. More...

bool	faudes::IsRelativelyOmegaClosed (const Generator &rGenPlant, const Generator &rGenCand)
	Test for relative closedness, omega languages. More...

bool	faudes::IsStdSynthesisConsistent (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rPlant0Gen)
	Test consistency of an abstractions w.r.t. More...

bool	faudes::IsStdSynthesisConsistent (const System &rPlantGen, const Generator &rPlant0Gen)
	Test consistency of an abstraction w.r.t standard synthesis. More...

bool	faudes::IsControllable (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSupCandGen)
	Test controllability. More...

bool	faudes::IsControllable (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSupCandGen, StateSet &rCriticalStates)
	Test controllability. More...

bool	faudes::IsControllable (const System &rPlantGen, const Generator &rSupCandGen)
	Test controllability. More...

void	faudes::SupConNB (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
	Nonblocking Supremal Controllable Sublanguage. More...

void	faudes::SupConNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
	Nonblocking Supremal Controllable Sublanguage. More...

void	faudes::SupConClosed (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
	Supremal Controllable and Closed Sublanguage. More...

void	faudes::SupConClosed (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
	Supremal Controllable and Closed Sublanguage. More...

bool	faudes::IsNormal (const Generator &rL, const EventSet &rOAlph, const Generator &rK)
	IsNormal: checks normality of a language K generated by rK wrt a language L generated by rL and the subset of observable events rOAlph. More...

bool	faudes::SupNorm (const Generator &rL, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
	SupNorm: compute supremal normal sublanguage. More...

bool	faudes::SupNormClosed (const Generator &rL, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
	SupNormClosed - compute supremal normal and closed sublanguage. More...

void	faudes::SupConNormClosed (const Generator &rL, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
	SupConNormClosed: compute supremal controllable, normal and closed sublanguage. More...

void	faudes::SupConNormNB (const Generator &rL, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rK, Generator &rResult)
	SupConNormNB: compute supremal controllable and normal sublanguage. More...

bool	faudes::SupReduce (const System &rPlantGen, const System &rSupGen, System &rReducedSup)
	Supervisor Reduction algorithm. More...

void	faudes::ComputeSynthObsEquiv (const Generator &rGenOrig, const EventSet &rConAlph, const EventSet &rLocAlph, std::map< Idx, Idx > &rMapStateToPartition, Generator &rResGen)
	Synthesis-observation equivalence. More...

void	faudes::SupTconNB (const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rFAlph, const EventSet &rPAlph, const Generator &rSpecGen, Generator &rResGen)
	Nonblocking Supremal TDES-Controllable Sublanguage. More...

void	faudes::SupTconNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
	Nonblocking Supremal TDES-Controllable Sublanguage. More...

bool	faudes::IsOmegaControllable (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSupCandGen)
	Test omega controllability. More...

bool	faudes::IsOmegaControllable (const System &rPlantGen, const Generator &rSupCandGen)
	Test omega-controllability. More...

void	faudes::SupConCmplClosed (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
	Supremal controllable and complete sublanguage. More...

void	faudes::SupConCmplClosed (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
	Supremal controllable and complete sublanguage. More...

void	faudes::SupConCmplNB (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
	Supremal controllable and complete sublanguage. More...

void	faudes::SupConCmplNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
	Supremal controllable and complete sublanguage. More...

void	faudes::SupConNormCmplNB (const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rSpecGen, Generator &rResGen)
	Supremal controllable, normal and complete sublanguage. More...

void	faudes::SupConNormCmplNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
	rti wrapper More...

void	faudes::OmegaSupConNB (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
	Omega-synthesis. More...

void	faudes::OmegaSupConNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
	Omega-synthesis. More...

void	faudes::OmegaConNB (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
	Omega-synthesis. More...

void	faudes::OmegaConNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
	Omega-synthesis. More...

void	faudes::OmegaSupConNormNB (const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rSpecGen, Generator &rResGen)
	Omega-synthesis for partial observation (experimental!) More...

void	faudes::OmegaSupConNormNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
	Omega-synthesis for partial observation. More...

void	faudes::OmegaConNormNB (const Generator &rPlantGen, const EventSet &rOAlph, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
	Omega-synthesis for partial observation (experimental!) More...

void	faudes::OmegaConNormNB (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
	Omega-synthesis for partial observation (experimental!) More...

Function Documentation

◆ CompositionalSynthesis()

FAUDES_API void faudes::CompositionalSynthesis	(	const GeneratorVector &	rPlantGenVec,
		const EventSet &	rConAlph,
		const GeneratorVector &	rSpecGenVec,
		std::map< Idx, Idx > &	rMapEventsToPlant,
		GeneratorVector &	rDisGenVec,
		GeneratorVector &	rSupGenVec
	)

Compositional synthesis.

This function implements controller synthesis for composed plants and composed specifications as discussed in "On Compostional Approaches for Discrete Event Systems Verification and Synthesis" Sahar Mohajerani, PhD, Sweden, 2015.

The present implementation was developed by Hao Zhou in course of his Master Thesis "Abstraktion und Komposition fuer den Entwurf ereignisdiskreter Regler", Erlangen, 2015. This particular variant throughs an exception on invalid input data; see also CompositionalSynthesisUnchecked(const GeneratorVector&,const EventSet&,const GeneratorVector&,std::map<Idx,Idx>&,GeneratorVector&,GeneratorVector&);

Parameters

rPlantGenVec	Plant components (must be deterministic)
rConAlph	Overall set of controllable events
rSpecGenVec	Specification components (must be deterministic)
rMapEventsToPlant	Resulting event map
rDisGenVec	Resulting distinuisher automata
rSupGenVec	Resulting supervisor automata

Definition at line 1379 of file syn_compsyn.cpp.

◆ ComputeSynthObsEquiv()

FAUDES_API void faudes::ComputeSynthObsEquiv	(	const Generator &	rGenOrig,
		const EventSet &	rConAlph,
		const EventSet &	rLocAlph,
		std::map< Idx, Idx > &	rMapStateToPartition,
		Generator &	rResGen
	)

Synthesis-observation equivalence.

Function to compute the coarsest synthesis-observation equivalence relation as proposed by Mohajerani, S., Malik, R. & Fabian, M. (2012). "Synthesis observation equivalence and weak synthesis observation equivalence", University of Waikato, Department of Computer Science. Compositional synthesis

The present implementation was developed by Hao Zhou in course of his Master Thesis "Abstraktion und Komposition fuer den Entwurf ereignisdiskreter Regler", Erlangen, 2015. Technically, the implementation is based on a previous variant of the bisimulation algorithm from the core library.

Parameters

rGenOrig	Generator under consideration
rConAlph	Set of controllable events
rLocAlph	Set of local events
rMapStateToPartition	Map original state to partition index
rResGen	Quotient generator

Definition at line 916 of file syn_synthequiv.cpp.

◆ IsControllable() [1/3]

FAUDES_API bool faudes::IsControllable	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const Generator &	rSupCandGen
	)

Test controllability.

Tests whether the candidate supervisor H is controllable w.r.t. the plant G. This implementation does not require the supervisor H to represent a sublanguage of the plant G.

Parameter restrictions: both generators must be deterministic and share the same alphabet.

Parameters

rPlantGen	Plant G
rCAlph	Controllable events
rSupCandGen	Supervisor candidate H

Exceptions

Exception

alphabets of generators don't match (id 100)
plant generator nondeterministic (id 201)
specification generator nondeterministic (id 203)
plant and Spec generator nondeterministic (id 204)

Returns: true / false

Definition at line 718 of file syn_supcon.cpp.

◆ IsControllable() [2/3]

FAUDES_API bool faudes::IsControllable	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const Generator &	rSupCandGen,
		StateSet &	rCriticalStates
	)

Test controllability.

Tests whether the candidate supervisor H is controllable w.r.t. the plant G. This implementation does not require the supervisor H to represent a sublanguage of the plant G.

If the candidate fails to be controllable, this version will return a set of "critical" states of the candidate supervisor. These states are characterised by (a) being reachable in the parallel composition of plant and supervisor (b) disabeling an uncontrollable transition of the plant Note: this was reimplemented in libFAUDES 2.20b.

Parameter restrictions: both generators must be deterministic and have the same alphabet.

Parameters

rPlantGen	Plant G
rCAlph	Controllable events
rSupCandGen	Supervisor candicate H
rCriticalStates	Set of critical states

Exceptions

Exception

alphabets of generators don't match (id 200)
plant generator nondeterministic (id 201)
specification generator nondeterministic (id 203)
plant and Spec generator nondeterministic (id 204)

Returns: true / false

Definition at line 740 of file syn_supcon.cpp.

◆ IsControllable() [3/3]

FAUDES_API bool faudes::IsControllable	(	const System &	rPlantGen,
		const Generator &	rSupCandGen
	)

Test controllability.

Tests whether the candidate supervisor h is controllable w.r.t. the plant g; this is a System wrapper for IsControllable

Parameters

rPlantGen	Plant g generator
rSupCandGen	Supervisor candidate h generator

Exceptions

Exception Alphabets of generators don't match (id 500) Plant generator nondeterministic (id 501) Specification generator nondeterministic (id 503) Plant & Spec generator nondeterministic (id 504)

Returns: true / false

Definition at line 885 of file syn_supcon.cpp.

◆ IsNormal()

FAUDES_API bool faudes::IsNormal	(	const Generator &	rL,
		const EventSet &	rOAlph,
		const Generator &	rK
	)

IsNormal: checks normality of a language K generated by rK wrt a language L generated by rL and the subset of observable events rOAlph.

This is done by checking if the following equality holds:

pinv(p(K)) intersect L \subseteq K

Thus, we assume K \subseteq L for a sufficient and necessary test.

Todos: check for efficient algorithm replacing above formula that returns false immediately after having found a non-normal string -> IsNormalFast(); implement test routines, verify correctness; compare performance with IsNormalAlt

Parameters

rL	generator of language L
rOAlph	observable alphabet
rK	generator of language K

Returns: true if K is normal w.r.t. L and OAlph

Exceptions

Exception

thrown by NormalityConsistencyCheck()

Definition at line 104 of file syn_supnorm.cpp.

◆ IsOmegaControllable() [1/2]

FAUDES_API bool faudes::IsOmegaControllable	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const Generator &	rSupCandGen
	)

Test omega controllability.

Tests whether the candidate supervisor H is omega controllable w.r.t. the plant G. This implementation invokes IsControllable and IsRelativelyOmegaClosed. A future implementation may be more efficient.

Parameter restrictions: both generators must be deterministic, omega-trim and have the same alphabet.

Parameters

rPlantGen	Plant G
rCAlph	Controllable events
rSupCandGen	Supervisor candidate H

Exceptions

Exception

Alphabets of generators don't match (id 100)
Arguments are not omega trim (id 201, only if FAUDES_CHECKED is set)
Arguments are non-deterministic (id 202, only if FAUDES_CHECKED is set)

Returns: true / false

Definition at line 42 of file syn_wsupcon.cpp.

◆ IsOmegaControllable() [2/2]

FAUDES_API bool faudes::IsOmegaControllable	(	const System &	rPlantGen,
		const Generator &	rSupCandGen
	)

Test omega-controllability.

Tests whether the candidate supervisor h is omega controllable w.r.t. the plant g; this is a System wrapper for IsOmegaControllable.

Parameters

rPlantGen	Plant g generator
rSupCandGen	Supervisor candidate h generator

Exceptions

Exception

Alphabets of generators don't match (id 100)
Arguments are not omega trim (id 201, only if FAUDES_CHECKED is set)
Arguments are non-deterministic (id 202, only if FAUDES_CHECKED is set)

Returns: true / false

Definition at line 107 of file syn_wsupcon.cpp.

◆ IsRelativelyMarked()

FAUDES_API bool faudes::IsRelativelyMarked	(	const Generator &	rGenPlant,
		const Generator &	rGenCand
	)

Test for relative marking.

Tests whether the language Lm(GCand) is relatively marked w.r.t. the language Lm(GPlant). The formal definition of this property requires

closure(Lm(GCand)) ^ Lm(GPlant) <= Lm(GCand).

The implementation tests

L(GCand) ^ Lm(GPlant) <= Lm(GCand)

by first performing the product composition and then inspecting the marking to require

( forall accessible (qPlant,qCand) ) [ qPlant in QPlant_m implies qCand in QCand_m ].

In general, the test is only sufficient. Provided the arguments are trim and deterministic, the test is sufficient and necessary.

Parameters

rGenPlant	Generator GPlant
rGenCand	Generator GCand

Exceptions

Exception

alphabets of generators don't match (id 100)
arguments are not trim (id 201, only if FAUDES_CHECKED is set)
arguments are non-deterministic (id 202, only if FAUDES_CHECKED is set)

Returns: true / false

Definition at line 43 of file syn_functions.cpp.

◆ IsRelativelyOmegaClosed()

FAUDES_API bool faudes::IsRelativelyOmegaClosed	(	const Generator &	rGenPlant,
		const Generator &	rGenCand
	)

Test for relative closedness, omega languages.

Tests whether the omega language Bm(GCand) is relatively closed w.r.t. the omega language Bm(GPlant). The formal definition of this property requires

closure(Bm(GCand)) ^ Bm(GPlant) = Bm(GCand).

The implementation first performs the product composition of the two generators with product state space QPlant x QCand and generated language L(GPlant x GCand) = L(GPlant) ^ L(GCand). It uses the composition to test the follwing three conditions:

L(GCand) subseteq L(GPlant);
no SCC of GPlant x GCand without GCand-marking contains a state with GPlant-marking; and
no SCC of GPlant x GCand without GPlant-marking contains a state with GCand-marking. If and only if all three tests are passed, the function returns true.

The arguments GCand and GPlant are required to be deterministic and omega trim.

Parameters

rGenPlant	Generator GPlant
rGenCand	Generator GCand

Exceptions

Exception

alphabets of generators don't match (id 100)
arguments are not omega trim (id 201, only if FAUDES_CHECKED is set)
arguments are non-deterministic (id 202, only if FAUDES_CHECKED is set)

Returns: true / false

Definition at line 396 of file syn_functions.cpp.

◆ IsRelativelyOmegaMarked()

FAUDES_API bool faudes::IsRelativelyOmegaMarked	(	const Generator &	rGenPlant,
		const Generator &	rGenCand
	)

Test for relative marking, omega langauges.

Tests whether the omega language Bm(GCand) is relatively marked w.r.t. the omega language Bm(GPlant). The formal definition of this property requires

closure(Bm(GCand)) ^ Bm(GPlant) <= Bm(GCand).

The implementation first performs the product composition of the two generators with product state space QPlant x QCand and generated language L(GPlant x GCand) = L(Plant) ^ L(Cand). It then investigates all SCCs that do not contain a state that corresponds to GCand-marking. If and only if none of the considered SCCs has a GPlant marking, the function returns true.

The arguments GCand and GPlant are required to be deterministic and omega trim.

Parameters

rGenPlant	Generator GPlant
rGenCand	Generator GCand

Exceptions

Exception

alphabets of generators don't match (id 100)
arguments are not omega-trim (id 201, only if FAUDES_CHECKED is set)
arguments are non-deterministic (id 202, only if FAUDES_CHECKED is set)

Returns: true / false

Definition at line 334 of file syn_functions.cpp.

◆ IsRelativelyPrefixClosed()

FAUDES_API bool faudes::IsRelativelyPrefixClosed	(	const Generator &	rGenPlant,
		const Generator &	rGenCand
	)

Test for relative prefix-closedness.

Tests whether the language Lm(GCand) is relatively closed w.r.t. the language Lm(GPant). The formal definition of this property requires

closure(Lm(GCand)) ^ Lm(GPlant) = Lm(GCand).

The implementation tests

L(GCand) ^ Lm(GPland) = Lm(GCand)

by performing the product composition and by testing

for L(GCand) subseteq L(GPlant), and
( forall accessible (qPland,qCand) ) [ qPlant in QPlant_m if and only if qCand in QCand_m ].

In general, the test is only sufficient. Provided the arguments are trim and deterministic, the test is sufficient and necessary.

Parameters

rGenPlant	Generator GPlant
rGenCand	Generator GCand

Exceptions

Exception

alphabets of generators don't match (id 100)
arguments are not trim (id 201, only if FAUDES_CHECKED is set)
arguments are non-deterministic (id 202, only if FAUDES_CHECKED is set)

Returns: true / false

Definition at line 97 of file syn_functions.cpp.

◆ IsStdSynthesisConsistent() [1/2]

FAUDES_API bool faudes::IsStdSynthesisConsistent	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const Generator &	rPlant0Gen
	)

Test consistency of an abstractions w.r.t.

standard controller synthesis.

Test whether abstraction-based supervisory controller design is guaranteed to lead to a non-blocking and controllable closed loop. This function implements the test proposed in "Moor, T.: Natural projections for the synthesis of non-conflicting supervisory controllers, Workshop on Discrete Event Systems (WODES), Paris, 2014".

Parameter restrictions: the generator has to be deterministic and the alphabets must match (see below for exceptions).

Parameters

rPlantGen	plant G
rCAlph	controllable events
rPlant0Gen	plant abstraction G0

Exceptions

Exception

the abstraction rPlant0Gen must have been obtained from the plant rPlantGen by natural projection (not tested)
the abstraction alphabet given by rPlant0Gen fails to be a subset of the overall alphabet given by rPlantGen (id 506)
alphabet with controllable Events fails be a subset of the abstraction alphabet given by rAbstrGen (id 506)
generators fail to be deterministic (id 501)

Returns: true / false

Definition at line 388 of file syn_sscon.cpp.

◆ IsStdSynthesisConsistent() [2/2]

bool faudes::IsStdSynthesisConsistent	(	const System &	rPlantGen,
		const Generator &	rPlant0Gen
	)

Test consistency of an abstraction w.r.t standard synthesis.

This is a convenience wrapprt for IsStdSynthesisConsistent(const Generator&, const EventSet&, const Generator&).

Parameters

rPlantGen	plant G incl. controllable events
rPlant0Gen	plant abstraction G0

Exceptions

Exception

the abstraction rPlant0Gen must have been obtained from the plant rPlantGen by natural projection (not tested)
the abstraction alphabet given by rPlant0Gen fails to be a subset of the overall alphabet given by rPlantGen (id 506)
alphabet with controllable Events fails be a subset of the abstraction alphabet given by rAbstrGen (id 506)
generators fail to be deterministic (id 501)

Returns: true / false

Definition at line 419 of file syn_sscon.cpp.

◆ OmegaConNB() [1/2]

FAUDES_API void faudes::OmegaConNB	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Omega-synthesis.

This procedure first computes the supremal omega-controllable sublanguage as proposed by J. Thistle, 1992, applied to the specific case of deterministoc Buechi automata. It then applies a control pattern to obtain a relatively topologically-closed result, i.e., the topological closure of the result can be used as a supervisor.

Parameter restrictions: both generators must be deterministic and have the same alphabet.

Parameters

rPlantGen	Plant G
rCAlph	Controllable events
rSpecGen	Specification Generator E
rResGen	Reference to resulting Generator to realize the closed-loop behaviour.

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)
spec nondeterministic (id 203)
plant and spec nondeterministic (id 204)

Definition at line 1627 of file syn_wsupcon.cpp.

◆ OmegaConNB() [2/2]

FAUDES_API void faudes::OmegaConNB	(	const System &	rPlantGen,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Omega-synthesis.

This is the RTI wrapper for
OmegaConNB(const Generator&, const EventSet&, const Generator&, Generator&). Controllability attributes are taken from the plant argument. If the result is specified as a System, attributes will be copied from the plant argument.

Parameters

rPlantGen	Plant System
rSpecGen	Specification Generator
rResGen	Reference to resulting Generator to realize the closed-loop behaviour.

Exceptions

Exception Alphabets of generators don't match (id 100) plant nondeterministic (id 201) spec nondeterministic (id 203) plant and spec nondeterministic (id 204)

Definition at line 1673 of file syn_wsupcon.cpp.

◆ OmegaConNormNB() [1/2]

FAUDES_API void faudes::OmegaConNormNB	(	const Generator &	rPlantGen,
		const EventSet &	rOAlph,
		const EventSet &	rCAlph,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Omega-synthesis for partial observation (experimental!)

Variation of supremal controllable prefix under partial observation. This variation applies a control pattern to obtain a relatively closed and omega-normal result. The latter properties are validated and an exception is thrown on an error. Thus, this function should not produce "false-positives". However, since it is derived from OmegaSupConNormNB(), is may return the empty languages even if a non-empty controller exists.

Parameter restrictions: both generators must be deterministic and have the same alphabet.

Parameters

rPlantGen	Plant G
rCAlph	Controllable events
rOAlph	Observable events
rSpecGen	Specification Generator E
rResGen	Reference to resulting Generator to realize the supremal closed-loop behaviour.

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)
spec nondeterministic (id 203)
plant and spec nondeterministic (id 204)

Definition at line 1737 of file syn_wsupcon.cpp.

◆ OmegaConNormNB() [2/2]

FAUDES_API void faudes::OmegaConNormNB	(	const System &	rPlantGen,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Omega-synthesis for partial observation (experimental!)

This is the RTI wrapper for
OmegaConNormNB(const Generator&, const EventSet&, const Generator&, Generator&). Controllability attributes are taken from the plant argument. If the result is specified as a System, attributes will be copied from the plant argument.

Parameters

rPlantGen	Plant System
rSpecGen	Specification Generator
rResGen	Reference to resulting Generator to realize the closed-loop behaviour.

Exceptions

Exception Alphabets of generators don't match (id 100) plant nondeterministic (id 201) spec nondeterministic (id 203) plant and spec nondeterministic (id 204)

Definition at line 1793 of file syn_wsupcon.cpp.

◆ OmegaSupConNB() [1/2]

FAUDES_API void faudes::OmegaSupConNB	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Omega-synthesis.

Computation of the supremal oemga-controllable sublanguage as proposed by Thistle/Wonham in "Control of w-Automata, Church's Problem, and the Emptiness Problem for Tree w-Automata", 1992, and, here, applied to the specific case of deterministic Buechi automata. In the given setting, the result matches the limit of the controllable prefix intersected with the plant and specification omega-languages.

Parameter restrictions: both generators must be deterministic and refer to the same alphabet.

Parameters

rPlantGen	Plant G
rCAlph	Controllable events
rSpecGen	Specification Generator E
rResGen	Reference to resulting Generator to realize the supremal closed-loop behaviour.

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)
spec nondeterministic (id 203)
plant and spec nondeterministic (id 204)

Definition at line 1588 of file syn_wsupcon.cpp.

◆ OmegaSupConNB() [2/2]

FAUDES_API void faudes::OmegaSupConNB	(	const System &	rPlantGen,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Omega-synthesis.

This is the RTI wrapper for
OmegaSupConNB(const Generator&, const EventSet&, const Generator&, Generator&). Controllability attributes are taken from the plant argument. If the result is specified as a System, attributes will be copied from the plant argument.

Parameters

rPlantGen	Plant System
rSpecGen	Specification Generator
rResGen	Reference to resulting Generator to realize the supremal closed-loop behaviour.

Exceptions

Exception Alphabets of generators don't match (id 100) plant nondeterministic (id 201) spec nondeterministic (id 203) plant and spec nondeterministic (id 204)

Definition at line 1606 of file syn_wsupcon.cpp.

◆ OmegaSupConNormNB() [1/2]

FAUDES_API void faudes::OmegaSupConNormNB	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const EventSet &	rOAlph,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Omega-synthesis for partial observation (experimental!)

Variation of supremal omega-controllable sublanguage to address normality requirements in the context of partial observation. The test used in this implementation is sufficient but not known to be necessary. Thus, the function may return only a subset of the relevant controllable prefix.

Parameter restrictions: both generators must be deterministic and have the same alphabet.

Parameters

rPlantGen	Plant G
rCAlph	Controllable events
rOAlph	Observable events
rSpecGen	Specification Generator E
rResGen	Reference to resulting Generator to realize the supremal closed-loop behaviour.

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)
spec nondeterministic (id 203)
plant and spec nondeterministic (id 204)

Definition at line 1695 of file syn_wsupcon.cpp.

◆ OmegaSupConNormNB() [2/2]

FAUDES_API void faudes::OmegaSupConNormNB	(	const System &	rPlantGen,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Omega-synthesis for partial observation.

This is the RTI wrapper for
OmegaSupConNormNB(const Generator&, const EventSet&, const Generator&, Generator&). Controllability attributes and observability attributes are taken from the plant argument. If the result is specified as a System, attributes will be copied from the plant argument.

Parameters

rPlantGen	Plant System
rSpecGen	Specification Generator
rResGen	Reference to resulting Generator to realize the supremal closed-loop behaviour.

Exceptions

Exception Alphabets of generators don't match (id 100) plant nondeterministic (id 201) spec nondeterministic (id 203) plant and spec nondeterministic (id 204)

Definition at line 1716 of file syn_wsupcon.cpp.

◆ SupConClosed() [1/2]

FAUDES_API void faudes::SupConClosed	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Supremal Controllable and Closed Sublanguage.

Given a closed plant language L and a closed specification E, this function computes a realisation of the supremal controllable and closed sublanguage of L^E. Arguments and result generate the respective language (i.e. marked languages are not considered.)

Parameter restrictions: both generators must be deterministic and have the same alphabet.

Parameters

rPlantGen	Plant L generated by rPlantGen
rCAlph	Controllable events
rSpecGen	Specification E generated rSpecGen
rResGen	Reference to resulting Generator, the minimal restrictive supervisor

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)
spec nondeterministic (id 203)
plant and spec nondeterministic (id 204)

Definition at line 778 of file syn_supcon.cpp.

◆ SupConClosed() [2/2]

FAUDES_API void faudes::SupConClosed	(	const System &	rPlantGen,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Supremal Controllable and Closed Sublanguage.

This is the RTI wrapper for
SupCon(const Generator&, const EventSet&, const Generator&, Generator&).

Controllability attributes are taken from the plant argument. If the result is specified as a System, attributes will be copied from the plant argument.

Parameters

rPlantGen	Plant System
rSpecGen	Specification Generator
rResGen	Reference to resulting Generator, the minimal restrictive supervisor

Exceptions

Exception Alphabets of generators don't match (id 100) plant nondeterministic (id 201) spec nondeterministic (id 203) plant and spec nondeterministic (id 204)

Definition at line 922 of file syn_supcon.cpp.

◆ SupConCmplClosed() [1/2]

FAUDES_API void faudes::SupConCmplClosed	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Supremal controllable and complete sublanguage.

Given a plant and a specification, this function computes a realisation of the supremal controllable and complete sublange. This version consideres the generated languages (ignores the marking). In particular, this implies that the result is prefix closed. It is returned as generated language.

Starting with a product composition of plant and specification, the implementation iteratively remove states that either contradict controllability or completeness. Removal of states is continued until no contradicting states are left. Thus, the result is indeed controllable and complete. The algorithm was proposed in

R. Kumar, V. Garg, and S.I. Marcus. On supervisory control of sequential behaviors. IEEE Transactions on Automatic Control, Vol. 37: pp.1978-1985, 1992.

The paper proves supremality of the result. Provided that the corresponding omega language of the specification is closed, the result of the above algorithm also realises the least restrictive closed loop behaviour of the corresponding omega language control problem.

Parameter restrictions: both generators must be deterministic and have the same alphabet. The result will be accessible and deterministic.

Parameters

rPlantGen	Plant G
rCAlph	Controllable events
rSpecGen	Specification Generator E
rResGen	Reference to resulting Generator

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)
spec nondeterministic (id 203)
plant and spec nondeterministic (id 204)

Definition at line 124 of file syn_wsupcon.cpp.

◆ SupConCmplClosed() [2/2]

FAUDES_API void faudes::SupConCmplClosed	(	const System &	rPlantGen,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Supremal controllable and complete sublanguage.

This is the RTI wrapper for
SupConCmplClosed(const Generator&, const EventSet&, const Generator&, Generator&). Controllability attributes are taken from the plant argument. If the result is specified as a System, attributes will be copied from the plant argument.

Parameters

rPlantGen	Plant System
rSpecGen	Specification Generator
rResGen	Reference to resulting Generator

Exceptions

Exception Alphabets of generators don't match (id 100) plant nondeterministic (id 201) spec nondeterministic (id 203) plant and spec nondeterministic (id 204)

Definition at line 182 of file syn_wsupcon.cpp.

◆ SupConCmplNB() [1/2]

FAUDES_API void faudes::SupConCmplNB	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Supremal controllable and complete sublanguage.

Given a plant and a specification, this function computes a realisation of the supremal controllable and complete sublange. This version consideres the marked languages.

Starting with a product composition of plant and specification, the implementation iteratively remove states that contradict controllability or completeness or that are not coaccessible. Removal of states is continued until no contradicting states are left. Thus, the result is indeed controllable, complete and coaccessible.

Considering the marked languages implies that only strings that simultanuosly reach a marking can survive the above procedure. From an omega-languages perspective, this is of limited use. However, in the special situation that the specification is relatively closed w.r.t. the plant, we can replace the specification by its prefix closure befor invoking SupConComplNB. In this situation we claim that the procedure returns a realisation of the the least restrictive closed loop behaviour of the corresponding omega language control problem.

Parameters

rPlantGen	Plant G
rCAlph	Controllable events
rSpecGen	Specification Generator E
rResGen	Reference to resulting Generator

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)
spec nondeterministic (id 203)
plant and spec nondeterministic (id 204)

Definition at line 209 of file syn_wsupcon.cpp.

◆ SupConCmplNB() [2/2]

FAUDES_API void faudes::SupConCmplNB	(	const System &	rPlantGen,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Supremal controllable and complete sublanguage.

This is the RTI wrapper for
SupConCmplNB(const Generator&, const EventSet&, const Generator&, Generator&). Controllability attributes are taken from the plant argument. If the result is specified as a System, attributes will be copied from the plant argument.

Parameters

rPlantGen	Plant System
rSpecGen	Specification Generator
rResGen	Reference to resulting Generator

Exceptions

Exception Alphabets of generators don't match (id 100) plant nondeterministic (id 201) spec nondeterministic (id 203) plant and spec nondeterministic (id 204)

Definition at line 269 of file syn_wsupcon.cpp.

◆ SupConNB() [1/2]

FAUDES_API void faudes::SupConNB	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Nonblocking Supremal Controllable Sublanguage.

Given a generator G (argument rPlantGen) and a specification language E (marked by argument rSpecGen), this procedures computes an automaton S such that Lm(S) is the supremal controllable sublanguage of Lm(G) ^ Lm(E) w.r.t. L(G). The result is given as a trim deterministic generator that may be used to supervise G in order to enforce E.

See "C.G CASSANDRAS AND S. LAFORTUNE. Introduction to Discrete Event Systems. Kluwer, 1999." for base algorithm.

Parameter restrictions: both generators must be deterministic and have the same alphabet.

Parameters

rPlantGen	Plant G
rCAlph	Controllable events
rSpecGen	Specification Generator to mark E
rResGen	Reference to resulting Generator, the minimal restrictive nonblocking supervisor

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)
spec nondeterministic (id 203)
plant and spec nondeterministic (id 204)

Definition at line 757 of file syn_supcon.cpp.

◆ SupConNB() [2/2]

FAUDES_API void faudes::SupConNB	(	const System &	rPlantGen,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Nonblocking Supremal Controllable Sublanguage.

This is the RTI wrapper for
SupConNB(const Generator&, const EventSet&, const Generator&, Generator&). Controllability attributes are taken from the plant argument. If the result is specified as a System, attributes will be copied from the plant argument.

Parameters

rPlantGen	Plant System
rSpecGen	Specification Generator
rResGen	Reference to resulting Generator, the minimal restrictive nonblocking supervisor

Exceptions

Exception Alphabets of generators don't match (id 100) plant nondeterministic (id 201) spec nondeterministic (id 203) plant and spec nondeterministic (id 204)

Definition at line 895 of file syn_supcon.cpp.

◆ SupConNormClosed()

FAUDES_API void faudes::SupConNormClosed	(	const Generator &	rL,
		const EventSet &	rCAlph,
		const EventSet &	rOAlph,
		const Generator &	rK,
		Generator &	rResult
	)

SupConNormClosed: compute supremal controllable, normal and closed sublanguage.

SupConNormClosed computes the supremal sublanguage of language K (generated by rK) that is

controllable w.r.t. the language L (generated by rL);
normal w.r.t. the language L; and
prefix closed.

The implementation is based on results by Brandt et al "Formulas for calculation supremal and normal sublanguages", Thm 4, System and Control Letters, 1990.

Parameters have to be deterministic, result is deterministic.

Parameters

rL	generates the closed language L=L(rL)
rCAlph	controllable alphabet
rOAlph	observable alphabet
rK	generates the closed language K=L(rK)
rResult	marks and generates the supremal contr, normal and closed sublanguage

Exceptions

Exception

Alphabets of generators don't match (id 500)
rCAlph not subset of rL.Alphabet() (id 506)
rOAlph not subset of rL.Alphabet() (id 506)
K is not subset of L. (id 0)

Definition at line 336 of file syn_supnorm.cpp.

◆ SupConNormCmplNB() [1/2]

FAUDES_API void faudes::SupConNormCmplNB	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const EventSet &	rOAlph,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Supremal controllable, normal and complete sublanguage.

SupConNormCmplNB computes the supremal sublanguage of language K (marked by rSpecGen) that

is controllable w.r.t. the language L (marked by rPlantGen);
has a prefix closure that is normal w.r.t. the closure of L
is complete

The implementation is based on an iteration by Yoo, Lafortune and Lin "A uniform approach for computing supremal sublanguages arising in supervisory control theory", 2002, further developped in Moor, Baier, Yoo, Lin, and Lafortune "On the computation of supremal sublanguages relevant to supervisory control, WODES 2012. The relationship to the supervision of omega languages under partial observation is discussed as an example in the WODES 2012 paper.

Parameters have to be deterministic, result is deterministic.

Parameters

rPlantGen	Plant L
rCAlph	Controllable events
rOAlph	Observable events
rSpecGen	Specification Generator E
rResGen	Reference to resulting Generator

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)
spec nondeterministic (id 203)
plant and spec nondeterministic (id 204)

Definition at line 295 of file syn_wsupcon.cpp.

◆ SupConNormCmplNB() [2/2]

FAUDES_API void faudes::SupConNormCmplNB	(	const System &	rPlantGen,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

rti wrapper

Supremal controllable, normal and complete sublanguage.

This is the RTI wrapper for
SupConNormCmplNB(const Generator&, const EventSet&, const EventSet&, const Generator&, Generator&). Event attributes are taken from the plant argument. If the result is specified as a System, attributes will be copied from the plant argument.

Parameters

rPlantGen	Plant System
rSpecGen	Specification Generator
rResGen	Reference to resulting Generator

Exceptions

Exception Alphabets of generators don't match (id 100) plant nondeterministic (id 201) spec nondeterministic (id 203) plant and spec nondeterministic (id 204)

Definition at line 336 of file syn_wsupcon.cpp.

◆ SupConNormNB()

FAUDES_API void faudes::SupConNormNB	(	const Generator &	rL,
		const EventSet &	rCAlph,
		const EventSet &	rOAlph,
		const Generator &	rK,
		Generator &	rResult
	)

SupConNormNB: compute supremal controllable and normal sublanguage.

SupConNormNB computes the supremal sublanguage of language K (marked by rK) that

is controllable w.r.t. the language L (marked by rL);
has a prefix closure that is normal w.r.t. the closure of L

The implementation is based on results by Yoo, Lafortune and Lin "A uniform approach for computing supremal sublanguages arising in supervisory control theory", 2002.

Parameters have to be deterministic, result is deterministic.

Parameters

rL	generates the closed language L=L(rL)
rCAlph	controllable alphabet
rOAlph	observable alphabet
rK	generates the closed language K=L(rK)
rResult	marks the supremal normal and controllable sublanguage

Exceptions

Exception

Alphabets of generators don't match (id 500)
rCAlph not subset of rL.Alphabet() (id 506)
rOAlph not subset of rL.Alphabet() (id 506)
K is not subset of L. (id 0)

Definition at line 376 of file syn_supnorm.cpp.

◆ SupNorm()

FAUDES_API bool faudes::SupNorm	(	const Generator &	rL,
		const EventSet &	rOAlph,
		const Generator &	rK,
		Generator &	rResult
	)

SupNorm: compute supremal normal sublanguage.

SupNorm calculates the supremal sublanguage of the closed language K (generated by rK) that is normal w.r.t. the closed language L (generated by rL) and the set of observable events.

Method: The supremal normal sublanguage is computed according to the Lin-Brandt-Formula: supnorm(K)wrt(L)=K-Pinv[P(L-K)]

SupNorm returns false on empty result.

Parameters have to be deterministic, result is deterministic.

Parameters

rL	generates the closed language L=L(rL)
rOAlph	observable alphabet
rK	generates the closed language K=L(rK)
rResult	marks the supremal normal sublanguage (not necessaryly prefix closed)

Returns: true for nonempty result

Exceptions

Exception

Alphabets of generators don't match (id 500)
rOAlph not subset of rL.Alphabet() (id 506)
K is not subset of L. (id 0)

Definition at line 234 of file syn_supnorm.cpp.

◆ SupNormClosed()

FAUDES_API bool faudes::SupNormClosed	(	const Generator &	rL,
		const EventSet &	rOAlph,
		const Generator &	rK,
		Generator &	rResult
	)

SupNormClosed - compute supremal normal and closed sublanguage.

SupNormClosed calculates the supremal sublanguage of the closed language K (generated by rK) that is closed and normal w.r.t. the closed language L (generated by rL) and the set of observable events.

Method: The supremal normal sublanguage is computed according to the Lin-Brandt-Formula: supnormclosed(K)wrt(L)=K-Pinv[P(L-K)]Sigma*

Parameters have to be deterministic, result is deterministic.

Parameters

rL	generates the closed language L=L(rL)
rOAlph	observable alphabet
rK	generates the closed language K=L(rK)
rResult	marks and generates the supremal normal and closed sublanguage

Returns: true for nonempty result

Exceptions

Exception

Alphabets of generators don't match (id 500)
rOAlph not subset of rL.Alphabet() (id 506)
K is not subset of L. (id 0)

Definition at line 287 of file syn_supnorm.cpp.

◆ SupReduce()

FAUDES_API bool faudes::SupReduce	(	const System &	rPlantGen,
		const System &	rSupGen,
		System &	rReducedSup
	)

Supervisor Reduction algorithm.

Computes a reduced supervisor from a given potentially non-reduced supervisor and the plant. This algorithm implements the results obtained in

R. Su and W. M. Wonham. Supervisor Reduction for Discrete-Event Systems. Discrete Event Dynamic Systems vol. 14, no. 1, January 2004.

Both, plant and supervisor MUST be deterministic and share the same alphabet!!!

Parameters

rPlantGen	Plant generator
rSupGen	Supervisor generator
rReducedSup	Reduced supervisor generator

Returns: True if a reduction was achieved

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)
supervisor nondeterministic (id 203)
plant and supervisor nondeterministic (id 204)

Definition at line 210 of file syn_supreduce.cpp.

◆ SupRelativelyPrefixClosed()

FAUDES_API void faudes::SupRelativelyPrefixClosed	(	const Generator &	rPlantGen,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Supremal Relatively Closed Sublanguage.

Computes the supremal sublanguage of the specification E that is relatively closed w.r.t. the plant G. The result is given as a trim deterministic generator that may be used as a specification for a subsequent controller design via SupConNB.

The implementation removes states from the product GxE that conflict with relative closedness. From the known formula supR(E)= (L^E) - (L-E)Sigma*, we know that the supremal sublanguage can be realized as a subautomaton of GxE. Thus, we conclude that our implementation indeed returns the supremum.

Parameter restrictions: both generators must be deterministic and have the same alphabet.

Parameters

rPlantGen	Plant G
rSpecGen	Specification Generator E
rResGen	Reference to resulting Generator

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)
spec nondeterministic (id 203)
plant and spec nondeterministic (id 204)

Definition at line 240 of file syn_functions.cpp.

◆ SupTconNB() [1/2]

FAUDES_API void faudes::SupTconNB	(	const Generator &	rPlantGen,
		const EventSet &	rCAlph,
		const EventSet &	rFAlph,
		const EventSet &	rPAlph,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Nonblocking Supremal TDES-Controllable Sublanguage.

Controllable sublanguage w.r.t. specified forcible and preemptable events. When the set of preemptable events consist exclusively of the tick event, this corresponds to TDES-controllability.

(!) Interface most likely to change — needs more testing/proper design (!)

Parameters

rPlantGen	Plant G
rCAlph	Controllable events
rFAlph	Forcible events
rPAlph	Premptable events
rSpecGen	Specification Generator E
rResGen	Reference to resulting Generator

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)
spec nondeterministic (id 203)
plant and spec nondeterministic (id 204)

Definition at line 274 of file syn_tsupcon.cpp.

◆ SupTconNB() [2/2]

FAUDES_API void faudes::SupTconNB	(	const System &	rPlantGen,
		const Generator &	rSpecGen,
		Generator &	rResGen
	)

Nonblocking Supremal TDES-Controllable Sublanguage.

This is the RTI wrapper for
SupTconNB(const Generator&, const EventSet&, const Generator&, Generator&). Controllability attributes are taken from the plant argument and tick is the only preemptable event. If the result is specified as a System, attributes will be copied from the plant argument.

(!) Interface most likely to change — needs more testing/ proper design (!)

Parameters

rPlantGen	Plant System
rSpecGen	Specification Generator
rResGen	Reference to resulting Generator, the minimal restrictive nonblocking supervisor

Exceptions

Exception Alphabets of generators don't match (id 100) plant nondeterministic (id 201) spec nondeterministic (id 203) plant and spec nondeterministic (id 204)

Definition at line 297 of file syn_tsupcon.cpp.

Detailed Description

License

Functions

Function Documentation

◆ CompositionalSynthesis()

◆ ComputeSynthObsEquiv()

◆ IsControllable() [1/3]

◆ IsControllable() [2/3]

◆ IsControllable() [3/3]

◆ IsNormal()

◆ IsOmegaControllable() [1/2]

◆ IsOmegaControllable() [2/2]

◆ IsRelativelyMarked()

◆ IsRelativelyOmegaClosed()

◆ IsRelativelyOmegaMarked()

◆ IsRelativelyPrefixClosed()

◆ IsStdSynthesisConsistent() [1/2]

◆ IsStdSynthesisConsistent() [2/2]

◆ OmegaConNB() [1/2]

◆ OmegaConNB() [2/2]

◆ OmegaConNormNB() [1/2]

◆ OmegaConNormNB() [2/2]

◆ OmegaSupConNB() [1/2]

◆ OmegaSupConNB() [2/2]

◆ OmegaSupConNormNB() [1/2]

◆ OmegaSupConNormNB() [2/2]

◆ SupConClosed() [1/2]

◆ SupConClosed() [2/2]

◆ SupConCmplClosed() [1/2]

◆ SupConCmplClosed() [2/2]

◆ SupConCmplNB() [1/2]

◆ SupConCmplNB() [2/2]

◆ SupConNB() [1/2]

◆ SupConNB() [2/2]

◆ SupConNormClosed()

◆ SupConNormCmplNB() [1/2]

◆ SupConNormCmplNB() [2/2]

◆ SupConNormNB()

◆ SupNorm()

◆ SupNormClosed()

◆ SupReduce()

◆ SupRelativelyPrefixClosed()

◆ SupTconNB() [1/2]

◆ SupTconNB() [2/2]