Detailed Description

License

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

Copyright (c) 2011, 2012, Tomas Masopust.

Functions
bool	faudes::ccTrim (const Generator &gen, Generator &trimGen)
	A more efficient Trim() operation. More...

bool	faudes::IsConditionalClosed (const GeneratorVector &specVect, const Generator &pk, const GeneratorVector &genVect, const Generator &gk)
	Conditionalclosedness Checking Algorithm. More...

bool	faudes::IsConditionalControllable (const GeneratorVector &specVect, const Generator &pk, const GeneratorVector &genVect, const Generator &gk, const EventSet &ACntrl)
	Conditionalcontrollability Checking Algorithm. More...

bool	faudes::IsConditionalDecomposable (const Generator &gen, const EventSetVector &ee, const EventSet &ek, Generator &proof)
	Conditionaldecomposability Checking Algorithm. More...

void	faudes::ConDecExtension (const Generator &gen, const EventSetVector &rAlphabets, EventSet &ek)
	Conditionaldecomposability Extension Algorithm. More...

bool	faudes::SupConditionalControllable (const Generator &gen, const GeneratorVector &genVector, const EventSet &ACntrl, const EventSet &InitEk, GeneratorVector &supVector, Generator &Coord)
	Conditionalcontrollability Checking Algorithm. More...

Function Documentation

◆ ccTrim()

FAUDES_API bool faudes::ccTrim	(	const Generator &	gen,
		Generator &	trimGen
	)

A more efficient Trim() operation.

Parameters

gen	The input generator to be trimmed
trimGen	The trimmed generator

Returns: True if the operation is successful

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)

Definition at line 221 of file con_cctrim.cpp.

◆ ConDecExtension()

FAUDES_API void faudes::ConDecExtension	(	const Generator &	gen,
		const EventSetVector &	rAlphabets,
		EventSet &	ek
	)

Conditionaldecomposability Extension Algorithm.

Given a language K over the union of alphabets, the algorithm extends the alphabet ek so that K is conditionally decomposable. This algorithm implements the results obtained in

J. Komenda, T. Masopust, J. H. van Schuppen. On Conditional Decomposability Preprint

The generator gen must be deterministic, and ek must contain the intersection of all subalphabets and be included in their union.

Parameters

gen	Generator representing the language K, i.e., Lm(gen)=K
rAlphabets	A vector of alphabets (at least two alphabets are required)
ek	The alhabet Ek that contains intersection of other alphabets and is included in their union

Returns: True Ek so that K is conditionally decomposible

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)

Definition at line 16 of file con_decomposability_extension.cpp.

◆ IsConditionalClosed()

FAUDES_API bool faudes::IsConditionalClosed	(	const GeneratorVector &	specVect,
		const Generator &	pk,
		const GeneratorVector &	genVect,
		const Generator &	gk
	)

Conditionalclosedness Checking Algorithm.

Checks whether a given language K is conditionally closed with respect to plants G_i, i=1,2,..,n. This algorithm implements the results obtained in

J. Komenda, T. Masopust, J. H. van Schuppen. Synthesis of controllable and normal sublanguages for discrete-event systems using a coordinator Systems & Control Letters 60(7), 492-502, 2011

K must be conditionally decomposable

Parameters

specVect	Vector of generators representing the specification languages P_{i+k}(K), i=1,2,..,n
pk	Generator for the coordinator part P_k(K)
genVect	Vecotr of generators for the plants G1,G2,..,Gn
gk	Generator for the coordinator Gk

Returns: True if K is conditionaly closed

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)

Definition at line 16 of file con_closed.cpp.

◆ IsConditionalControllable()

FAUDES_API bool faudes::IsConditionalControllable	(	const GeneratorVector &	specVect,
		const Generator &	pk,
		const GeneratorVector &	genVect,
		const Generator &	gk,
		const EventSet &	ACntrl
	)

Conditionalcontrollability Checking Algorithm.

Checks whether a given language K over the union of alphabets is conditionally controllable with respect to the plant G. This algorithm implements the results obtained in

J. Komenda, T. Masopust, J. H. van Schuppen. Synthesis of Safe Sublanguages satisfying Global Specification using Coordination Scheme for Discrete-Event Systems WODES 2010

K must be conditionally decomposable

Parameters

specVect	Vector of generators representing the specification languages P_{i+k}(K), i=1,2,..,n
pk	Generator for the coordinator part P_k(K)
genVect	Vecotr of generators for the plants G1,G2,..,Gn
gk	Generator for the coordinator Gk
ACntrl	Event set of all controllable events

Returns: True if K is conditionaly controllable

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)

Definition at line 16 of file con_controllability.cpp.

◆ IsConditionalDecomposable()

FAUDES_API bool faudes::IsConditionalDecomposable	(	const Generator &	gen,
		const EventSetVector &	ee,
		const EventSet &	ek,
		Generator &	proof
	)

Conditionaldecomposability Checking Algorithm.

Checks whether a given language K over the union of alphabets is conditionally decomposable with respect to these alphabets and ek. This algorithm implements the results obtained in

J. Komenda, T. Masopust, J. H. van Schuppen. On Nonblockingness and Conditional Decomposability Manuscript

The generator gen must be deterministic, and ek must contain the intersection of all subalphabets and be included in their union.

Parameters

gen	Generator representing the language K, i.e., Lm(gen)=K
ee	A vector of alphabets (at least two alphabets are required)
ek	The alhabet Ek that contains intersection of other alphabets and is included in their union
proof	A generator which gives the proof that the language K is NOT conditionally decomposable

Returns: True if K is conditionaly decomposible

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)

Definition at line 16 of file con_decomposability.cpp.

◆ SupConditionalControllable()

FAUDES_API bool faudes::SupConditionalControllable	(	const Generator &	gen,
		const GeneratorVector &	genVector,
		const EventSet &	ACntrl,
		const EventSet &	InitEk,
		GeneratorVector &	supVector,
		Generator &	Coord
	)

Conditionalcontrollability Checking Algorithm.

Computation of the supremal conditionally controllable sublanguage of a given language K with respect to the plant G. This algorithm implements the results obtained in

J. Komenda, T. Masopust, J. H. van Schuppen. Synthesis of Safe Sublanguages satisfying Global Specification using Coordination Scheme for Discrete-Event Systems WODES 2010 (and its Automatica version)

Parameters

gen	Generator for the specification language K
genVector	Vector of generators for the plants G1,G2,..,Gn
ACntrl	Controllable events
InitEk	evenset
supVector	Vector of generators; supervisors supC_{i+k} such that \|\|supC_{i+k} is the supremal conditionally controllable sublanguage of K are returned in this vector
Coord	a generator; computed coordinator is returned in this parameter

Returns: Returns the supVector of supervisors and the computer coordinator

Exceptions

Exception

alphabets of generators don't match (id 100)
plant nondeterministic (id 201)

Definition at line 18 of file con_supcc.cpp.

Detailed Description

License

Functions

Function Documentation

◆ ccTrim()

◆ ConDecExtension()

◆ IsConditionalClosed()

◆ IsConditionalControllable()

◆ IsConditionalDecomposable()

◆ SupConditionalControllable()