Observer PlugIn

Detailed Description

Overview

This plugin offers algorithms for the verification and synthesis of natural projections that are observers according to

K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

and that fulfill the output control consistency (OCC) or local control consistency (LCC) condition for maximally permissive hierarchical control according to

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.

License

The initial version of the observer plug-in was implemented by Bernd Opitz together with the initial version of libFAUDES. A major revision and extension was part of Christian Breindl's student project, supervised by Klaus Schmidt. The observer plugin is distributed with libFAUDES and under the terms of the LGPL.

Copyright (c) 2006, Bernd Opitz
Copyright (c) 2008, Christian Breindl, Klaus Schmidt.

Functions
bool	faudes::IsMutuallyControllable (const System &rGen1, const System &rGen2)
	Verification of mutual controllability. More...
Idx	faudes::calcClosedObserver (const Generator &rGenObs, EventSet &rHighAlph)
	L(G)-observer computation by adding events to the high-level alphabet. More...
Int	faudes::calcNaturalObserver (const Generator &rGenObs, EventSet &rHighAlph)
	Lm(G)-observer computation by adding events to the high-level alphabet. More...
Int	faudes::calcNaturalObserverLCC (const Generator &rGen, const EventSet &rControllableEvents, EventSet &rHighAlph)
	Lm(G)-observer computation including local control consistency (LCC) by adding events to the high-level alphabet. More...
Int	faudes::calcMSAObserver (const Generator &rGen, EventSet &rHighAlph)
	MSA-observer computation by adding events to the high-level alphabet. More...
Int	faudes::calcMSAObserverLCC (const Generator &rGen, const EventSet &rControllableEvents, EventSet &rHighAlph)
	MSA-observer computation including local control consistency (LCC) by adding events to the high-level alphabet. More...
FAUDES_API void	faudes::ExtendHighAlphabet (const Generator &rGenObs, EventSet &rHighAlph, std::map< Idx, Idx > &rMapStateToPartition)
	Extension of the high-level alphabet to achieve the Lm-observer property. More...
FAUDES_API void	faudes::calcAbstAlphClosed (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
	L(G)-observer computation. More...
FAUDES_API void	faudes::calcAbstAlphObs (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
	Lm-observer computation. More...
FAUDES_API void	faudes::calcAbstAlphMSA (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
	MSA-observer computation. More...
FAUDES_API void	faudes::calcAbstAlphObsLCC (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
	Lm-observer computation including local control consistency (LCC). More...
FAUDES_API void	faudes::calcAbstAlphMSALCC (System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
	MSA-observer computation including local control consistency (LCC). More...
bool	faudes::IsObs (const Generator &rLowGen, const EventSet &rHighAlph)
	Verification of the natural observer property. More...
bool	faudes::IsMSA (const Generator &rLowGen, const EventSet &rHighAlph)
	Verification of the MSA observer property. More...
bool	faudes::IsOCC (const System &rLowGen, const EventSet &rHighAlph)
	Verification of output control consistency (OCC). More...
bool	faudes::IsLCC (const System &rLowGen, const EventSet &rHighAlph)
	Verification of local control consistency (LCC). More...
void	faudes::calcAbstAlphObs (MtcSystem &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, std::map< Idx, std::set< Idx > > &rMapRelabeledEvents)
	Lm-observer computation. More...

Function Documentation

calcAbstAlphClosed()

FAUDES_API void faudes::calcAbstAlphClosed	(	System &	rGenObs,
		EventSet &	rHighAlph,
		EventSet &	rNewHighAlph,
		std::map< Idx, std::set< Idx > > &	rMapRelabeledEvents
	)

L(G)-observer computation.

This function modifies a given generator and an associated natural projection such that the resulting natural projection is an L(G)-observer for the prefix-closed language of the resulting generator. This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

The alphabet rHighAlph has to be a subset of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEvents	Maps the original events to sets of newly introduced events (accumulatoive, call clear before)

Example: Computation of an L(G)-observer

Generator with relabeled events Original high-level alphabet (rHighAlph): alpha, beta, gamma

Result of calcAbstAlphClosed(rGenObs, rHighAlph, rNewHighAlph, rMapRelabeledEvents); New high-level alphabet (rNewHighAlph): alpha, beta, gamma, aNewHLevent_1, eNewHLevent_1, hNewHLevent_1

Definition at line 667 of file op_observercomputation.cpp.

calcAbstAlphMSA()

FAUDES_API void faudes::calcAbstAlphMSA	(	System &	rGenObs,
		EventSet &	rHighAlph,
		EventSet &	rNewHighAlph,
		std::map< Idx, std::set< Idx > > &	rMapRelabeledEvents
	)

MSA-observer computation.

This function modifies a given generator and an associated natural projection such that the resulting natural projection is an msa-observer for the language marked by the resulting generator. This function evaluates the msa-observer algorithm as described in K. Schmidt and Th. Moor, "Marked String Accepting Observers for the Hierarchical and Decentralized Control of Discrete Event Systems," Workshop on Discrete Event Systems, 2006.

The alphabet rHighAlph has to be a subset of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEvents	Maps the original events to sets of newly introduced events (accumulatoive, call clear before)

Example: Computation of an MSA-observer

Generator with relabeled events Original high-level alphabet (rHighAlph): alpha, beta, gamma

Result of calcAbstAlphObs(rGenObs, rHighAlph, rNewHighAlph, rMapRelabeledEvents); New high-level alphabet (rNewHighAlph): alpha, beta, gamma, aNewHLevent_1, eNewHLevent_1, hNewHLevent_1

Definition at line 825 of file op_observercomputation.cpp.

calcAbstAlphMSALCC()

FAUDES_API void faudes::calcAbstAlphMSALCC	(	System &	rGenObs,
		EventSet &	rHighAlph,
		EventSet &	rNewHighAlph,
		std::map< Idx, std::set< Idx > > &	rMapRelabeledEvents
	)

MSA-observer computation including local control consistency (LCC).

This function modifies a given generator and an associated natural projection such that the resulting natural projection is an MSA-observer for the language marked by the resulting generator and at the same time fulfills the local control consistency condition (LCC). This function evaluates the msa-observer algorithm as described in 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. with an extension to LCC as indicated in 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.

The alphabet rHighAlph has to be a subset of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEvents	Maps the original events to sets of newly introduced events (accumulatoive, call clear before)

Example: Computation of an MSA-observer with local control consistency (LCC)

Generator with relabeled events Original high-level alphabet (rHighAlph): alpha, beta, gamma

Result of calcAbstAlphObsLCC(rGenObs, rHighAlph, rNewHighAlph, rMapRelabeledEvents); New high-level alphabet (rNewHighAlph): alpha, beta, gamma, d, f, h, aNewHLevent_2, bNewHLevent_1, cNewHLevent_1, eNewHLevent_2, hNewHLevent_2

Definition at line 1245 of file op_observercomputation.cpp.

calcAbstAlphObs() [1/2]

void faudes::calcAbstAlphObs	(	MtcSystem &	rGenObs,
		EventSet &	rHighAlph,
		EventSet &	rNewHighAlph,
		std::map< Idx, std::set< Idx > > &	rMapRelabeledEvents
	)

Lm-observer computation.

This function modifies a given generator and an associated natural projection such that the resulting natural projection is an Lm-observer for the language marked by the resulting generator. This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

The alphabet rHighAlph has to be a subset of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEvents	Maps the original events to sets of newly introduced events (accumulatoive, call clear before)

Definition at line 60 of file mtc_observercomputation.cpp.

calcAbstAlphObs() [2/2]

FAUDES_API void faudes::calcAbstAlphObs	(	System &	rGenObs,
		EventSet &	rHighAlph,
		EventSet &	rNewHighAlph,
		std::map< Idx, std::set< Idx > > &	rMapRelabeledEvents
	)

Lm-observer computation.

This function modifies a given generator and an associated natural projection such that the resulting natural projection is an Lm-observer for the language marked by the resulting generator. This function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004.

The alphabet rHighAlph has to be a subset of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEvents	Maps the original events to sets of newly introduced events (accumulatoive, call clear before)

Example: Computation of an Lm(G)-observer

Generator with relabeled events Original high-level alphabet (rHighAlph): alpha, beta, gamma

Result of calcAbstAlphObs(rGenObs, rHighAlph, rNewHighAlph, rMapRelabeledEvents); New high-level alphabet (rNewHighAlph): alpha, beta, gamma, aNewHLevent_1, eNewHLevent_1, hNewHLevent_1

Definition at line 746 of file op_observercomputation.cpp.

calcAbstAlphObsLCC()

FAUDES_API void faudes::calcAbstAlphObsLCC	(	System &	rGenObs,
		EventSet &	rHighAlph,
		EventSet &	rNewHighAlph,
		std::map< Idx, std::set< Idx > > &	rMapRelabeledEvents
	)

Lm-observer computation including local control consistency (LCC).

This function modifies a given generator and an associated natural projection such that the resulting natural projection is an Lm-observer for the language marked by the resulting generator and at the same time fulfills the local control consistency condition (LCC). The function evaluates the observer algorithm as described in K. C. Wong and W. M. Wonham, "On the Computation of Observers in Discrete Event Systems," Discrete Event Dynamic Systems, vol. 14, no. 1, pp. 55-107, 2004. with an extension to LCC as indicated in 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.

The alphabet rHighAlph has to be a subset of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rHighAlph	Initial abstraction alphabet
rNewHighAlph	Modified abstraction alphabet such that the abstraction is an Lm-observer
rMapRelabeledEvents	Maps the original events to sets of newly introduced events (accumulatoive, call clear before)

Example: Computation of an Lm(G)-observer with local control consistency (LCC)

Generator with relabeled events Original high-level alphabet (rHighAlph): alpha, beta, gamma

Result of calcAbstAlphObsLCC(rGenObs, rHighAlph, rNewHighAlph, rMapRelabeledEvents); New high-level alphabet (rNewHighAlph): alpha, beta, gamma, d, f, h, aNewHLevent_2, bNewHLevent_1, cNewHLevent_1, eNewHLevent_2, hNewHLevent_2

Definition at line 1171 of file op_observercomputation.cpp.

calcClosedObserver()

FAUDES_API Idx faudes::calcClosedObserver	(	const Generator &	rGenObs,
		EventSet &	rHighAlph
	)

L(G)-observer computation by adding events to the high-level alphabet.

This function extends a given high-level alphabet such that the resulting natural projection is an L(G)-observer for the prefix-closed language of the given generator. This function evaluates the natural observer algorithm as described in Lei Feng; Wonham, W.M., "On the Computation of Natural Observers in Discrete-Event Systems," Decision and Control, 2006 45th IEEE Conference on , vol., no., pp.428-433, 13-15 Dec. 2006

The alphabet rHighAlph has to be a subset of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rHighAlph	Reference to the initial abstraction alphabet that is modified by the algorithm

Returns

number of states of the high-level generator

Example: Computation of an L(G)-observer

Original generator Original high-level alphabet (rHighAlph): alpha, gamma

Result of calcClosedObserver(rGenObs, rHighAlph); New high-level alphabet (rHighAlph): alpha, beta, gamma, h

Definition at line 413 of file op_observercomputation.cpp.

calcMSAObserver()

FAUDES_API Int faudes::calcMSAObserver	(	const Generator &	rGen,
		EventSet &	rHighAlph
	)

MSA-observer computation by adding events to the high-level alphabet.

This function extends a given high-level alphabet such that the resulting natural projection is an MSA-observer for the marked language of the given generator. This function adapts the natural observer algorithm as described in Lei Feng; Wonham, W.M., "On the Computation of Natural Observers in Discrete-Event Systems," Decision and Control, 2006 45th IEEE Conference on , vol., no., pp.428-433, 13-15 Dec. 2006 to the msa-obsever property.

The alphabet rHighAlph has to be a subset of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters

rGen	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rHighAlph	Reference to the initial abstraction alphabet that is modified by the algorithm

Returns

number of states of the high-level generator

Example: Computation of an msa-observer

Original generator Original high-level alphabet (rHighAlph): alpha, gamma

Result of calcMSAObserver(rGenObs, rHighAlph); New high-level alphabet (rHighAlph): alpha, beta, gamma, h

Definition at line 476 of file op_observercomputation.cpp.

calcMSAObserverLCC()

FAUDES_API Int faudes::calcMSAObserverLCC	(	const Generator &	rGen,
		const EventSet &	rControllableEvents,
		EventSet &	rHighAlph
	)

MSA-observer computation including local control consistency (LCC) by adding events to the high-level alphabet.

This function extends a given high-level alphabet such that the resulting natural projection is an MSA-observer and locally control consistent (lcc) for the marked language of the given generator. This function adapts the natural observer algorithm as described in Lei Feng; Wonham, W.M., "On the Computation of Natural Observers in Discrete-Event Systems," Decision and Control, 2006 45th IEEE Conference on , vol., no., pp.428-433, 13-15 Dec. 2006 to the msa-obsever property and uses LCC as defined in 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.

The alphabet rHighAlph has to be a subset of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters

rGen	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rControllableEvents
rHighAlph	Reference to the initial abstraction alphabet that is modified by the algorithm

Returns

number of states of the high-level generator

Example: Computation of an msa-observer with LCC

Original generator Original high-level alphabet (rHighAlph): alpha, gamma; controllable events: a, f, g, h

Result of calcMSAObserverLCC(rGenObs, rControllableEvents, rHighAlph); New high-level alphabet (rHighAlph): alpha, beta, gamma, a, e, f, g, h

Definition at line 497 of file op_observercomputation.cpp.

calcNaturalObserver()

FAUDES_API Int faudes::calcNaturalObserver	(	const Generator &	rGenObs,
		EventSet &	rHighAlph
	)

Lm(G)-observer computation by adding events to the high-level alphabet.

This function extends a given high-level alphabet such that the resulting natural projection is an Lm(G)-observer for the marked language of the given generator. This function evaluates the natural observer algorithm as described in Lei Feng; Wonham, W.M., "On the Computation of Natural Observers in Discrete-Event Systems," Decision and Control, 2006 45th IEEE Conference on , vol., no., pp.428-433, 13-15 Dec. 2006

The alphabet rHighAlph has to be a subset of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rHighAlph	Reference to the initial abstraction alphabet that is modified by the algorithm

Returns

number of states of the high-level generator

Example: Computation of an Lm(G)-observer

Original generator Original high-level alphabet (rHighAlph): alpha, gamma

Result of calcNaturalObserver(rGenObs, rHighAlph); New high-level alphabet (rHighAlph): alpha, beta, gamma, delta, h

Definition at line 433 of file op_observercomputation.cpp.

calcNaturalObserverLCC()

FAUDES_API Int faudes::calcNaturalObserverLCC	(	const Generator &	rGen,
		const EventSet &	rControllableEvents,
		EventSet &	rHighAlph
	)

Lm(G)-observer computation including local control consistency (LCC) by adding events to the high-level alphabet.

This function extends a given high-level alphabet such that the resulting natural projection is an Lm(G)-observer and locally control consistent (lcc) for the marked language of the given generator. This function evaluates the natural observer algorithm as described in Lei Feng; Wonham, W.M., "On the Computation of Natural Observers in Discrete-Event Systems," Decision and Control, 2006 45th IEEE Conference on , vol., no., pp.428-433, 13-15 Dec. 2006 and uses LCC as defined in K. Schmidt and C. Breindl, "On Maximal Permissiveness of Hierarchical and Modular Supervisory Control Approaches for Discrete Event Systems

The alphabet rHighAlph has to be a subset of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters

rGen	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rHighAlph	Reference to the initial abstraction alphabet that is modified by the algorithm
rControllableEvents

Returns

number of states of the high-level generator

Example: Computation of an Lm(G)-observer with LCC

Original generator Original high-level alphabet (rHighAlph): alpha, gamma; controllable events: a, f, g, h

Result of calcNaturalObserverLCC(rGenObs, rControllableEvents, rHighAlph); New high-level alphabet (rHighAlph): alpha, beta, gamma, delta, a, e, f, g, h

Definition at line 454 of file op_observercomputation.cpp.

ExtendHighAlphabet()

FAUDES_API void faudes::ExtendHighAlphabet	(	const Generator &	rGenObs,
		EventSet &	rHighAlph,
		std::map< Idx, Idx > &	rMapStateToPartition
	)

Extension of the high-level alphabet to achieve the Lm-observer property.

This algorithm extends the given high-level alphabet such that nondeterminism and unobservable transitions in the quotient automaton computed with the current high-level alphabet are removed. The function is called by calcNaturalObserver.

The alphabet rHighAlph has to be a subset of the alphabet of rGenObs. rGenObs must be a deterministic generator. There are no further restrictions on parameters.

Parameters

rGenObs	Low-level generator. It is modified by the algorithm by relabeling transitions and events
rHighAlph	Reference to the initial abstraction alphabet that is modified by the algorithm
rMapStateToPartition	Map from states in rGenObs to states (partitions) in the computed quotient automaton

Definition at line 520 of file op_observercomputation.cpp.

IsLCC()

FAUDES_API bool faudes::IsLCC	(	const System &	rLowGen,
		const EventSet &	rHighAlph
	)

Verification of local control consistency (LCC).

For verifying if a natural projection fulfills the local control consistency condition, a backward reachability is conducted. If starting from a state, where an uncontrollable high-level event is feasible, at least one local state cannot be reached by an uncontrollable path, LCC is violated.

Parameters

rLowGen	Input System
rHighAlph	High level alphabet

Returns

true if LCC holds

Definition at line 157 of file op_obserververification.cpp.

IsMSA()

FAUDES_API bool faudes::IsMSA	(	const Generator &	rLowGen,
		const EventSet &	rHighAlph
	)

Verification of the MSA observer property.

For verifying if a natural projection has the marked string accepting observer property, one step in the MSA observer algorithm is evaluated. If the resulting generator equals the input generator, then the natural projection on the abstraction alphabet is an MSA observer.

Parameters

rLowGen	Input generator
rHighAlph	High level alphabet

Returns

true if the MSA observer property holds

Definition at line 62 of file op_obserververification.cpp.

IsMutuallyControllable()

FAUDES_API bool faudes::IsMutuallyControllable	(	const System &	rGen1,
		const System &	rGen2
	)

Verification of mutual controllability.

This function checks if two generators are mutually controllable w.r.t. each other. A definition of mutual controllability is given in S.-H. Lee and K. C. Wong, “Structural decentralised control of concurrent DES,” European Journal of Control, vol. 35, pp. 1125-1134,2002.

Parameters

rGen1	Generator 1
rGen2	Generator 2

Returns

True if mutual controllability is fulfilled

Example:

Violation of mutual controllability

rGen1	rGen2

Mutual controllability is fulfilled

rGen3	rGen2

Definition at line 32 of file op_mc.cpp.

IsObs()

FAUDES_API bool faudes::IsObs	(	const Generator &	rLowGen,
		const EventSet &	rHighAlph
	)

Verification of the natural observer property.

For verifying if a natural projection has the observer property, one step in the observer algorithm is evaluated. If the resulting generator equals the input generator, then the natural projection on the abstraction alphabet is an observer.

Parameters

rLowGen	Input generator
rHighAlph	High level alphabet

Returns

true if the observer property holds

Definition at line 38 of file op_obserververification.cpp.

IsOCC()

FAUDES_API bool faudes::IsOCC	(	const System &	rLowGen,
		const EventSet &	rHighAlph
	)

Verification of output control consistency (OCC).

For verifying if a natural projection fulfills the output control consistency condition, a backward reachability is conducted. If starting from a state, where an uncontrollable high-level event is feasible, a controllable event can be reached on a local backward path, OCC is violated.

Parameters

rLowGen	Input System
rHighAlph	High level alphabet

Returns

true if OCC holds

Definition at line 86 of file op_obserververification.cpp.