|
|
||||||
|
|
Statespace ConversionNote. Functions in this section maintain event attributes, provided that they match for all arguments. DeterministicPowerset construction to enforce determinism. 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:
Parameter Conditions:The resulting generator is deterministic. IsDeterministicTest for determinsim. 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:
UniqueInitEnforce unique initial state. 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. StateMinStateset minimization. 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:
Parameter Conditions:The argument must be deterministic and so will be the result. libFAUDES 2.32b --- 2024.03.08 --- with "synthesis-observer-diagnosis-iosystem-hiosys-multitasking-coordinationcontrol-timed-iodevice-simulator-luabindings" |