Awali
Another Weighted Automata library

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...  
Contains functions related to automata/transducer quotient (in particular, minimisation.
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
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. 
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.
aut  
opts  A set of options; QUOTIENT_ALGO is meaningful. 
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.
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. 