Quotient

Contains functions related to automata/transducer quotient (in particular, minimisation. More...

Functions
automaton_t	awali::dyn::coquotient (automaton_t aut, std::vector< std::vector< state_t >> &equiv, options_t opts={})
	Computes the coquotient of an automaton with respect to a given equivalence. More...
automaton_t	awali::dyn::min_coquotient (automaton_t aut, options_t opts={})
	Computes the minimal coquotient of aut. More...
automaton_t	awali::dyn::quotient (automaton_t aut, std::vector< std::vector< state_t >> &equiv, options_t opts={})
	Computes the quotient of an automaton with respect to a given equivalence. More...

Detailed Description

Contains functions related to automata/transducer quotient (in particular, minimisation.

Function Documentation

coquotient()

automaton_t awali::dyn::coquotient	(	automaton_t	aut,
		std::vector< std::vector< state_t >> &	equiv,
		options_t	opts = {}
	)

Computes the coquotient of an automaton with respect to a given equivalence.

Simply calls transpose , quotient, transpose

Parameters

aut	The automaton whose states should be merged
equiv	The congruence of mergible states
opts	A set of options; only SAFE is meaningful. If SAFE is true, a test will be performed to verify that equiv is indeed a congruence.

Returns

A new automaton with states merged

min_coquotient()

automaton_t awali::dyn::min_coquotient	(	automaton_t	aut,
		options_t	opts = {}
	)

Computes the minimal coquotient of aut.

Simply calls transpose, then min_quotient, then transpose.

Parameters

aut
opts	A set of options; QUOTIENT_ALGO is meaningful.

Returns

A new automaton.

quotient()

automaton_t awali::dyn::quotient	(	automaton_t	aut,
		std::vector< std::vector< state_t >> &	equiv,
		options_t	opts = {}
	)

Computes the quotient of an automaton with respect to a given equivalence.

This function merges the states w.r.t. the partition given as second argument.

Argument equiv must be a partition: the vectors of states must be disjoint and their union must span over all the states. Only the outgoing transitions of the first state of each part are considered to build the quotient. As a consequence, the result of this function is meaningful only if all equivalent states have the same successors (modulo equiv). A check of this is done unless opts sets SAFE to false.

Param equiv is described as the list of its parts, each part being a list of states; equiv can be partially described: if a state does not appear in any part, it is considered as a singleton part.

Parameters

aut	The automaton whose states should be merged
equiv	The congruence of mergible states
opts	A set of options; only SAFE is meaningful. If SAFE is true, a test will be performed to verify that equiv is indeed a congruence.

Returns

A new automaton with states merged