Omega Automata Plug-In

Detailed Description

The omega-automata plug-in collects data structures and functions to support supervisory control of non-termination processes.

License

The omega-automata plugin is distributed with libFAUDES and under the terms of the LGPL.

Copyright (c) 2025 Thomas Moor.

Classes
class	faudes::RabinPair
class	faudes::RabinAcceptance

Functions
bool	faudes::IsBuechiControllable (const Generator &rGenPlant, const EventSet &rCAlph, const Generator &rGenCand)
bool	faudes::IsBuechiControllable (const System &rPlantGen, const Generator &rCandGen)
void	faudes::SupBuechiCon (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
void	faudes::SupBuechiCon (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
void	faudes::BuechiCon (const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
void	faudes::BuechiCon (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
void	faudes::SupBuechiConNorm (const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rSpecGen, Generator &rResGen)
void	faudes::SupBuechiConNorm (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
void	faudes::BuechiConNorm (const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rSpecGen, Generator &rResGen)
void	faudes::BuechiConNorm (const System &rPlantGen, const Generator &rSpecGen, Generator &rResGen)
bool	faudes::BuechiTrim (vGenerator &rGen)
bool	faudes::BuechiTrim (const vGenerator &rGen, vGenerator &rRes)
void	faudes::BuechiProduct (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
void	faudes::aBuechiProduct (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
void	faudes::BuechiParallel (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
void	faudes::aBuechiParallel (const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
void	faudes::BuechiClosure (Generator &rGen)
bool	faudes::IsBuechiClosed (const Generator &rGen)
void	faudes::ExportHoa (std::ostream &rOutStream, const Generator &rAut, SymbolTable *pSymTab)
void	faudes::ExportHoa (const std::string &rFilename, const Generator &rAut, SymbolTable *pSymTab)
void	faudes::ImportHoa (std::istream &rInStream, RabinAutomaton &rAut, const SymbolTable *pSymTab, bool resolve, bool trace)
void	faudes::ImportHoa (const std::string &rFilename, RabinAutomaton &rAut, const SymbolTable *pSymTab, bool resolve, bool trace)
void	faudes::RabinCtrlPfx (const RabinAutomaton &rRAut, const EventSet &rSigmaCtrl, StateSet &rCtrlPfx)
void	faudes::RabinLiveStates (const TransSet &rTransRel, const TransSetX2EvX1 &rRevTransRel, const RabinPair &rRPair, StateSet &rInv)
void	faudes::RabinLiveStates (const vGenerator &rRAut, const RabinPair &rRPair, StateSet &rInv)
void	faudes::RabinLiveStates (const RabinAutomaton &rRAut, StateSet &rInv)
void	faudes::RabinTrimSet (const RabinAutomaton &rRAut, StateSet &rTrim)
bool	faudes::RabinTrim (RabinAutomaton &rRAut)
bool	faudes::RabinTrim (const RabinAutomaton &rRAut, RabinAutomaton &rRes)
void	faudes::RabinBuechiAutomaton (const RabinAutomaton &rRAut, const Generator &rBAut, RabinAutomaton &rRes)
void	faudes::RabinBuechiProduct (const RabinAutomaton &rRAut, const Generator &rBAut, RabinAutomaton &rRes)

Function Documentation

aBuechiParallel()

FAUDES_API void faudes::aBuechiParallel	(	const Generator &	rGen1,
		const Generator &	rGen2,
		Generator &	rResGen
	)

Parallel composition with relaxed acceptance condition.

See also BuechiParallel(const Generator&, const Generator&, Generator&). This version tries to be transparent on event attributes: if argument attributes match and if the result can take the respective attributes, then they are copied; it is considered an error if argument attributes do not match.

Parameters

rGen1	First generator
rGen2	Second generator
rResGen	Reference to resulting composition generator

Definition at line 525 of file omg_buechifnct.cpp.

aBuechiProduct()

FAUDES_API void faudes::aBuechiProduct	(	const Generator &	rGen1,
		const Generator &	rGen2,
		Generator &	rResGen
	)

Product composition for Buechi automata

See also BuechiProduct(const Generator&, const Generator&, Generator&). This version tries to be transparent on event attributes: if argument attributes match and if the result can take the respective attributes, then they are copied; it is considered an error if argument attributes do not match.

Parameters

rGen1	First generator
rGen2	Second generator
rResGen	Reference to resulting product composition generator

Definition at line 288 of file omg_buechifnct.cpp.

BuechiClosure()

FAUDES_API void faudes::BuechiClosure

(

Generator &

rGen

)

Topological closure.

This function computes the topological closure the omega language Bm accepted by the Buechi automaton rGen.

Method: First, BuechiTrim is called to erase all states of rGen that do not contribute to Bm. Then, all remaining states are marked.

No restrictions on parameter.

Parameters

rGen	Generator that realizes Bm to which omega closure is applied

Example:

Generator G	BuechiClosure(G)

Definition at line 70 of file omg_buechifnct.cpp.

BuechiCon() [1/2]

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

Omega-synthesis w.r.t. Buechi accptance

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 1380 of file omg_buechictrl.cpp.

BuechiCon() [2/2]

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

Omega-synthesis

This is the RTI wrapper for
BuechiCon(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 1426 of file omg_buechictrl.cpp.

BuechiConNorm() [1/2]

FAUDES_API void faudes::BuechiConNorm	(	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 SupBuechiConNorm(), 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 1490 of file omg_buechictrl.cpp.

BuechiConNorm() [2/2]

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

Omega-synthesis for partial observation (experimental!)

This is the RTI wrapper for
BuechiConNorm(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 1546 of file omg_buechictrl.cpp.

BuechiParallel()

FAUDES_API void faudes::BuechiParallel	(	const Generator &	rGen1,
		const Generator &	rGen2,
		Generator &	rResGen
	)

Parallel composition with relaxed acceptance condition.

This version of the parallel composition relaxes the synchronisation of the acceptance condition (marking). It requires that the omega extension of the generated language has infinitely many prefixes that comply to the marked languages of G1 and G2, referring to the projection on the respective alphabet. It does however not require the synchronous acceptance.

Parameters

rGen1	First generator
rGen2	Second generator
rResGen	Reference to resulting parallel composition generator

Definition at line 316 of file omg_buechifnct.cpp.

BuechiProduct()

FAUDES_API void faudes::BuechiProduct	(	const Generator &	rGen1,
		const Generator &	rGen2,
		Generator &	rResGen
	)

Product composition for Buechi automata

Referring to the Buechi acceptance condition, the resulting genarator accepts all those inifinite words that are accepted by both, G1 and G2. This implementation extends the usual product state space by a flag to indentify executions with alternating marking.

Parameters

rGen1	First generator
rGen2	Second generator
rResGen	Reference to resulting product composition generator

Definition at line 166 of file omg_buechifnct.cpp.

BuechiTrim() [1/2]

FAUDES_API bool faudes::BuechiTrim	(	const vGenerator &	rGen,
		vGenerator &	rRes
	)

Trim generator w.r.t Buechi acceptance

This is a API wrapper for BuechiTrim(vGenerator&).

Parameters

rGen	Automaton to trim (const ref)
rRes	Resulting automaton

Returns

True if resulting generator contains at least one initial state and at least one marked state.

Definition at line 54 of file omg_buechifnct.cpp.

BuechiTrim() [2/2]

FAUDES_API bool faudes::BuechiTrim

(

vGenerator &

rGen

)

Trim generator w.r.t Buechi acceptance

This function removes states such that the generator becomes omega trim while not affecting the induced omega language.

The implementation first makes the generator accessible and then iteratively removes state that either never reach a marked state or that are guaranteed to eventually reach a terminal state. There might be a more efficient approach.

Parameters

rGen	Automaton to trim

Returns

True if resulting generator contains at least one initial state and at least one marked state.

Definition at line 34 of file omg_buechifnct.cpp.

ExportHoa() [1/2]

FAUDES_API void faudes::ExportHoa	(	const std::string &	rFilename,
		const Generator &	rAut,
		SymbolTable *	pSymTab = nullptr
	)

Export Automaton as HOA formated stream

Convenience wrapper, for detail see ExportHoa(std::ostream&, const Generator&)

Parameters

rFilename	File to write to
rAut	Automaton to write
pSymTab	Optional symbol table to record event mapping

Definition at line 150 of file omg_hoa.cpp.

ExportHoa() [2/2]

FAUDES_API void faudes::ExportHoa	(	std::ostream &	rOutStream,
		const Generator &	rAut,
		SymbolTable *	pSymTab = nullptr
	)

Export Automaton as HOA formated stream

We iterate over all relevant entities of the specified automaton and somewhat adboc writes HOA formated entities to the specified stream.

Our current implementation is restricted to (nondetermistic) Buechi automata.

Parameters

rOutStream	Stream to write to
rAut	Automaton to write
pSymTab	Optional symbol table to record event mapping

Definition at line 133 of file omg_hoa.cpp.

ImportHoa() [1/2]

FAUDES_API void faudes::ImportHoa	(	const std::string &	rFilename,
		RabinAutomaton &	rAut,
		const SymbolTable *	pSymTab = nullptr,
		bool	resolve = false,
		bool	trace = false
	)

Import Automaton from HOA formated file

Convenience wrapper, see ImportHoa(std::istream&,RabinAutomaton&) for details.

Parameters

rFilename	File to read from
rAut	Resultimg automaton
pSymTab	Optional symbol table to provide event mapping
resolve	Ask cpphoafparser to resolve aliase
trace	Ask cpphoafparser for a parse trace on std::cerr

Definition at line 387 of file omg_hoa.cpp.

ImportHoa() [2/2]

FAUDES_API void faudes::ImportHoa	(	std::istream &	rInStream,
		RabinAutomaton &	rAut,
		const SymbolTable *	pSymTab = nullptr,
		bool	resolve = false,
		bool	trace = false
	)

Import Automaton from HOA formated stream

To reading input in HAO format we use the cpphoafparser library, authored/copyrighted by

Joachim Klein klein.nosp@m.@tcs.nosp@m..inf..nosp@m.tu-d.nosp@m.resde.nosp@m.n.de DDavid Mueller david.nosp@m..mue.nosp@m.ller@.nosp@m.tcs..nosp@m.inf.t.nosp@m.u-dr.nosp@m.esden.nosp@m..de

We have found the original sources at

http://automata.tools/hoa/cpphoafparser

They are distributed under LGPL v2.1 conditions and we include them with libFAUDES under the same license terms.

Our current implementation can read deterministic Rabin automata with implicit edges. This is not a restriction of cpphoafparser and we extend for further use cases in future.

Parameters

rInStream	Stream to read from
rAut	Resultimg automaton
pSymTab	Optional symbol table to provide event mapping
resolve	Ask cpphoafparser to resolve aliase
trace	Ask cpphoafparser for a parse trace on std::cerr

Definition at line 364 of file omg_hoa.cpp.

IsBuechiClosed()

FAUDES_API bool faudes::IsBuechiClosed

(

const Generator &

rGen

)

Test for topologically closed omega language.

This function tests whether the omega language Bm(G) realized by the specified Buechi automata is topologically closed.

Method: First, compute the Buechi-trim state set and restrict the discussion to that set. Then, omega-closedness is equivalent to the non-existence on a non-trivial SCC with no marked states.

Parameters

rGen	Generator that realizes Bm to which omega closure is applied

Returns

True <> Bm(G) is omega closed

Definition at line 84 of file omg_buechifnct.cpp.

IsBuechiControllable() [1/2]

FAUDES_API bool faudes::IsBuechiControllable	(	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, where omega-languages are interpreted by Buechi acceptance condition. This implementation invokes IsControllable and IsBuechiRelativelyClosed. 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 40 of file omg_buechictrl.cpp.

IsBuechiControllable() [2/2]

FAUDES_API bool faudes::IsBuechiControllable	(	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 105 of file omg_buechictrl.cpp.

RabinBuechiAutomaton()

FAUDES_API void faudes::RabinBuechiAutomaton	(	const RabinAutomaton &	rRAut,
		const Generator &	rBAut,
		RabinAutomaton &	rRes
	)

Construct Rabin-Buechi automata.

Given two automata rRAut and rBAut, this function constructs the accessible product state set and corresponding syncronizsed transitions. For the generated languages, this is exactly the same as the common product operation. It then lifts the two individual acceptance conditions to the product state set. If both rRAut and rBAut are full, so is the result. In that case, the result accepts by its Rabin acceptance condition runs that are accepted by rRAut and by its Buechi acceptance condition those path thet are accepted by rBAut.

The intended use case is when rRAut is a liveness specification and rBAut is a plant with liveness guarantees.

Parameters

rRAut	Rabin automaton
rBAut	Buechi automaton
rRes	Resulting product automaton

Definition at line 188 of file omg_rabinfnct.cpp.

RabinBuechiProduct()

FAUDES_API void faudes::RabinBuechiProduct	(	const RabinAutomaton &	rRAut,
		const Generator &	rBAut,
		RabinAutomaton &	rRes
	)

Product composition for a Rabin automaton with a Buechi automaton

Referring to each acceptance condition specified by rRAut and rBAut, the resulting Rabin automaton accepts all those runs, that are accepted by both rRAut and rBAut. To support supervisory control, this function sets the marking of the result as a lifted variant of rBAut.

This implementation extends the usual product state space by a flag to indentify executions with alternating marking. This restricts the applicability to one Rabin pair only. Future revisions may drop this restriction.

Parameters

rRAut	First automaton
rBAut	Second automaton
rRes	Reference to resulting product composition

Definition at line 269 of file omg_rabinfnct.cpp.

RabinCtrlPfx()

FAUDES_API void faudes::RabinCtrlPfx	(	const RabinAutomaton &	rRAut,
		const EventSet &	rSigmaCtrl,
		StateSet &	rCtrlPfx
	)

Controllability prefix for Rabin automata.

Computation of the controllability prefix as proposed by Thistle/Wonham in "Supervision of infinite behavior of Discrete Event Systems, 1994, using the fixpoint iteration from "Control of w-Automata, Church's Problem, and the Emptiness Problem for Tree w-Automata", 1992.

Parameters

rRAut	Automaton to control
rSigmaCtrl	Set of controllable events
rCtrlPfx	State set that marks the controllability prefix.

Definition at line 358 of file omg_rabinctrl.cpp.

RabinLiveStates() [1/3]

FAUDES_API void faudes::RabinLiveStates	(	const RabinAutomaton &	rRAut,
		StateSet &	rInv
	)

Live states w.r.t a Rabin acceptance condition.

Iterates over all Rabin pairs and Returns the union of all live states.

Parameters

rRAut	Trasition system to operate on
rInv	Resulting set of live states

Definition at line 125 of file omg_rabinfnct.cpp.

RabinLiveStates() [2/3]

void faudes::RabinLiveStates	(	const TransSet &	rTransRel,
		const TransSetX2EvX1 &	rRevTransRel,
		const RabinPair &	rRPair,
		StateSet &	rInv
	)

Live states w.r.t a Rabin pair.

A state is considered live if it allows for a future path that such that the acceptance condition is met,

The implementation is along the following line

• initialise LSet the ISet
• run a nu iteration on LSet to figure the largest existential invariant
• run a mu iteration on LSet*RSet to restrict LSet to states which can reach RSet
• repeat the last to steps until a fix point is attained
• run one more mu iteration on LSet to extend to the bachward reach

Parameters

rTransRel	Trasition systej to operate on
rRevTransRel	Reverse sorted variant
rRPair	Rabin pair to consider
rInv	Resulting set of live states

Definition at line 34 of file omg_rabinfnct.cpp.

RabinLiveStates() [3/3]

FAUDES_API void faudes::RabinLiveStates	(	const vGenerator &	rRAut,
		const RabinPair &	rRPair,
		StateSet &	rInv
	)

Live states w.r.t a Rabin pair.

API wrapper.

Parameters

rRAut	Trasition system to operate on
rRPair	Rabin pair to consider
rInv	Resulting set of live states

Definition at line 111 of file omg_rabinfnct.cpp.

RabinTrim() [1/2]

FAUDES_API bool faudes::RabinTrim	(	const RabinAutomaton &	rRAut,
		RabinAutomaton &	rRes
	)

Trim generator w.r.t Rabin acceptance

Restrict the automaton to the set of trim states; see also RaibLiveStates and RabinTrimSet

Parameters

rRAut	Automaton to trim
rRes	Resulting trimmed automaton

Returns

True if resulting generator contains at least one initial state.

Definition at line 180 of file omg_rabinfnct.cpp.

RabinTrim() [2/2]

FAUDES_API bool faudes::RabinTrim

(

RabinAutomaton &

rRAut

)

Trim generator w.r.t Rabin acceptance

Restrict the automaton to the set of trim states; see also RaibLiveStates and RabinTrimSet

Parameters

rRAut

Automaton to trim

Returns

True if resulting generator contains at least one initial state.

Definition at line 153 of file omg_rabinfnct.cpp.

RabinTrimSet()

FAUDES_API void faudes::RabinTrimSet	(	const RabinAutomaton &	rRAut,
		StateSet &	rTrim
	)

Trim generator w.r.t. Rabin acceptance

This function computes the set of states that contribute to the accepted omega language. The current implementation returns the union of all states that are live w.r.t. a Rabin pair, restricted to reachable states.

Parameters

rRAut	Automaton to consider
rInv	Resulting set of trim statess

Definition at line 144 of file omg_rabinfnct.cpp.

SupBuechiCon() [1/2]

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

Omega-synthesis w.r.t. Buechi acceptance condition

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 1341 of file omg_buechictrl.cpp.

SupBuechiCon() [2/2]

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

Omega-synthesis w.r.t. Buechi acceptance

This is the RTI wrapper for
SupBuchiCon(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 1359 of file omg_buechictrl.cpp.

SupBuechiConNorm() [1/2]

FAUDES_API void faudes::SupBuechiConNorm	(	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 presumably to necessary. Thus, the function in general 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 1448 of file omg_buechictrl.cpp.

SupBuechiConNorm() [2/2]

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

Omega-synthesis for partial observation (experimental!)

This is the RTI wrapper for
SupBuechiConNorm(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 1469 of file omg_buechictrl.cpp.