Misc Functions on Generators

EmptyLanguage

Set generator to mark empty language.

Signature:

EmptyLanguage(+In+ EventSet Sigma, +Out+ Generator GRes)

Detailed description:

Returns a generator G with the specified alphabet Sigma, no states and no transitions; i.e., we have Lm(G) = L(G) = 0.

Parameter Conditions:

The empty language generator is deterministic.

IsEmptyLanguage

Test Generator G for empty marked language Lm(G).

Signature:

IsEmptyLanguage(+In+ Generator GArg, +Out+ Boolean BRes)

Parameter Conditions:

The argument may be non-deterministic.

Automaton

Convert generator to formal automaton.

Signature:

Automaton(+InOut+ Generator GArg)

Automaton(+InOut+ Generator GArg, +In+ EventSet Sigma)

Detailed description:

Converts the given generator G to a formal automaton that generates the same marked language Lm(G) while accepting any input string, i.e. L(G) = Sigma*. This is achieved by introducing a dump state to represent Sigma*-Closure(Lm(G)).

Example:
G GRes
Parameter Conditions:

The provided generator is assumed to be deterministic. The resulting generator is guaranteed to be deterministic.

IsPrefixClosed

Tests a language for being prefix-closed.

Signature:

IsPrefixClosed(+In+ Generator G, +Out+ Boolean BRes)

Detailed description:

A language L is prefix-closed if for each string  L all prefixes r ≤ s are also element of L:

 L and r ≤ s        r  L.

The function IsPrefixClosed tests whether the language Lm(G) marked by the specified generator G is prefix-closed. It does so by testing whether any state that is accessible and co-accessible also is marked. For deterministic generators, this condition is sufficient and necessary. In general, it is only sufficient.

Example:
G

The language Lm(G) marked by the above generator is not prefix-closed, since the states 1, 2 and 4 are accessible and co-accessible but not marked. For example, the string ac  Lm(G) is a prefix of acbb  Lm(G).

PrefixClosure

Compute prefix closure for given language.

Signature:

PrefixClosure(+InOut+ Generator GArg)

Detailed description:

For any language L there exists a smallest prefix-closed superset, the so-called prefix-closure of L:

Closure(L) := {r  Sigma*|  s  L : r ≤ s}.

This function computes a realisation of the prefix-closure of Lm(GArg) by first erasing all states that are not co-accessible and then marking the remaining states.

Example:
G GRes

IsOmegaClosed

Tests a language for being omega-closed.

Signature:

IsOmegaClosed(+In+ Generator G, +Out+ Boolean BRes)

Detailed description:

A omega-language  Sigma^w is omega-closed if any strictly increasing sequence of prefixes from L converges to an omega-string in L, i.e. if

L = B(Prefix(L)),

where Prefix(L)  Sigma* denotes the set of all finite prefixes from L and B(.) is the adherence operator.

The function IsOmegaClosed tests for the specified generator G whether Bm(G) is omega-closed. The implementation first computes the omega-trim state set. If within this set there exists an SCC with no marked states the function returns false. Else it returns true.

Example:
G

The language Bm(G) realized by the above generator is not omega-closed. The states 6 and 7 constitute an SCC when restricting G to the omega-trim state set {1,2,4,6,7}. Thus, the limit of the sequence a d (a b)^i is in B(Prefix(L)) but not in B(L). The function IsOmegaClosed returns false.

Parameter Conditions:

The argument must be deterministic.

OmegaClosure

Compute omega closure for given language.

Signature:

OmegaClosure(+InOut+ Generator GArg)

Detailed description:

For any omega-language  Sigma^w there exists a smallest omega-closed superset, the so-called omega-closure or topological closure of L:

Closure(L) = B(Prefix(L))  Sigma^w,

where Prefix(H)  Sigma* denotes the set of all finite prefixes from H and B(.) is the limit operator ; see also IsOmegaClosed.

The function OmegaClosure computes a realisation of the the omega-closure for the specified omega language Bm(GArg). It first invokes OmegaTrim and then markes all states. Thus, Closure(Bm(GArg)) = B(GRes) = Bm(GRes) and Prefix(Bm(GArg)) = L(GRes) = Lm(GRes).

Example:
G GRes

libFAUDES 2.32b --- 2024.03.01 --- with "synthesis-observer-observability-diagnosis-hiosys-iosystem-multitasking-coordinationcontrol-timed-simulator-iodevice-luabindings-hybrid-example-pybindings"