Statespace Conversion

Note. Functions in this section maintain event attributes, provided that they match for all arguments.

Deterministic

Powerset construction to enforce determinism.

Signature:

Deterministic(+In+ Generator G, +Out+ Generator GRes)

Detailed description:

The so called powerset- or subset-construction converts the specified generator to a deterministic generator without affecting marked and generated language. The state space of the resulting generator is a reachable subset of the powerset of the original state set. Indeed, the computational worst case is characterised by exponential growth of the number of states. See [C3] for the basic algorithm.

Example:
G GRes
Parameter Conditions:

The resulting generator is deterministic.

IsDeterministic

Test for determinsim.

Signature:

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

Detailed description:

A generator is deterministic if it has no more than one initial state and if the transition relation is a partial function. Formally:

|Q0| ≤ 1, and
( q  Q, o  Sigma )[    |delta(q,o)| ≤ 1    ].

Note: previous versions of libFAUDES also required |Q0| = 1. This turned out not practical for functions that operate on the generated language as opposed to the marked language.

UniqueInit

Enforce unique initial state.

Signature:

UniqueInit(+InOut+ Generator G)

UniqueInit(+In+ Generator G, +Out+ Generator GRes)

Detailed description:

If the argument generator has precisely one initial state, this function does nothing. Else, this function introduces a new and unique initial state and relinks transitions accordinly. If the argument generator used to have more than one initial state, this operation may render the output nondeterministic. If the argument generator used to have no initial state, the output generator will generate the empty string language as opposed to the empty language. Otherwise, generated and marked languages are preserved.

Note: call this function followed by Deterministic to convert the generator to a deterministic generator with exactly one initial state.

StateMin

Stateset minimization.

Signature:

StateMin(+In+ Generator GArg, +Out+ Generator GRes)

StateMin(+InOut+ Generator G)

Detailed description:

Constructs a generator with minimal stateset while preserving the generated and marked languages. This function implements the (n*log n) set partitioning algorithm by John E. Hopcroft, e.g. [C3]. The original algorithm expects an accessible input generator, the implementation will convert the argument if necessary.

Example:
G GRes
Parameter Conditions:

The argument must be deterministic and so will be the result.

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