Separation by group languages. More...

#include "graphs_tarjan.h"
#include "nfa.h"
#include "nfa_intersec.h"
#include "printing.h"
#include "type_dlist.h"
#include "type_partitions.h"
#include "flint/fmpz.h"
#include "flint/fmpz_mat.h"
#include <stdbool.h>
#include <stdlib.h>

Classes
struct	num_span_forest
	Type used to store the information needed to solve AMT-separation on the SCCs of a dgraph. More...

Functions
bool	solve_system_amt (fmpz_mat_t MAT, int *target, uint nb_rows, uint nb_cols)

num_span_forest *	compute_span_forest (dgraph G, parti sccs, bool *allowed)
	Computes a spanning forest from a dgraph.

void	delete_span_forest (num_span_forest *forest)
	Deletes the structure used to store the spanning forest.

parti *	dgraph_amt_fold (dgraph g, parti sccs)
	Computes the folding of a dgraph according to the AMT-separation.

void	compute_amt_kernel_regular (morphism , bool , uint *)
	Computes the regular elements of the AMT-kernel in a morphism (non-regular elements are ignored).

void	build_hnf_matrix_two (dgraph g1, dgraph g2, num_span_forest span1, num_span_forest span2, uint q1, uint q2, fmpz_mat_t MAT)

void	compute_amt_pairs_regular (morphism M, num_span_forest rspan, num_span_forest lspan, uint e, uint f, dequeue first, dequeue *second)
	Computes the anti AMT-pairs (q,t) where q is in the R-class of e and t is in the L-class of f.

parti *	dgraph_stal_fold (dgraph G, parti sccs, basis ba)
	Computes the Stalling partition obtained from a dgraph.

dgraph *	shrink_mod (dgraph g, parti fold, parti *sccs)
	Computes the graph obtained by folding a right or left Cayley graph according to the Stalling partition. Modulo mode: the alphabet is reduced to a single letter.

dgraph *	shrink_mod_mirror (dgraph g, parti fold, parti *sccs)
	Computes the graph obtained by folding a right or left Cayley graph according to the Stalling partition. Modulo mode: the alphabet is reduced to a single letter. Mirror mode: the transitions are reversed.

dgraph *	shrink_grp (dgraph g, parti fold, parti *sccs)
	Computes the graph obtained by folding a right or left Cayley graph according to the Stalling partition. Group mode: the alphabet is preserved.

dgraph *	shrink_grp_mirror (dgraph g, parti fold, parti *sccs)
	Computes the graph obtained by folding a right or left Cayley graph according to the Stalling partition. Group mode: the alphabet is preserved. Mirror mode: the transitions are reversed.

dgraph *	dgraph_implement_fold (dgraph g, parti sccs, parti *fold)
	Folds a single SCC of a dgraph according to a folding partition generated from MOD, AMT or GR.

dfa *	dfa_compute_folding (dfa *A, basis ba)

parti *	nfa_inv_ext (nfa *)
	Computation of the inverse transitions inside the SCCs of an NFA.

void	nfa_remove_inv (nfa *)
	Remove all inverse transitions in an NFA.

parti *	nfa_stal_fold (nfa , parti )
	Computation of the partition obtained by the Stallings folding in SCCs.

nfa *	nfa_dyck_ext (nfa , parti )
	Computation of the NFA used in the group separation algorithm by adding epsilon transitions between pairs of states connected by a word in the Dyck language.

bool	decid_grp_sep (nfa , nfa , bool, FILE *)
	GR-separation.

nfa *	nfa_proj_unary (nfa *)
	Projection of a NFA over a one-letter alphabet.

bool	decid_mod_sep (nfa , nfa , bool, FILE *)
	MOD-separation.

bool	decid_st_sep (nfa , nfa , FILE *)
	ST-separation.

Detailed Description

Separation by group languages.

Function Documentation

◆ compute_amt_kernel_regular()

void compute_amt_kernel_regular	(	morphism *	M,
		bool *	mono_in_sub,
		uint *	size )

Computes the regular elements of the AMT-kernel in a morphism (non-regular elements are ignored).

Parameters

M	The morphism.
mono_in_sub	The array to fill with the elements of the kernel.
size	Used to return the size of the kernel.

◆ compute_amt_pairs_regular()

void compute_amt_pairs_regular	(	morphism *	M,
		num_span_forest *	rspan,
		num_span_forest *	lspan,
		uint	e,
		uint	f,
		dequeue *	first,
		dequeue *	second )

Computes the anti AMT-pairs (q,t) where q is in the R-class of e and t is in the L-class of f.

Parameters

M	The morphism.
rspan	The spanning forest of the R-classes
lspan	The spanning forest of the L-classes
e	The idempotent e.
f	The idempotent f.
first	The dequeue to fill with the first elements of each anti-pair.
second	The dequeue to fill with the second elements of each anti-pair.

◆ compute_span_forest()

num_span_forest * compute_span_forest	(	dgraph *	G,
		parti *	sccs,
		bool *	allowed )

Computes a spanning forest from a dgraph.

Remarks: The sccs are not mandatory. If a NULL pointer is given, it is assumed that the dgraph consists of a single SCC (if this is not the case, the result is undefined) and the returned forest will contain a single tree whose root is the first state of the dgraph.

Returns: The spanning forest.

Parameters

G	The dgraph
sccs	The partition into SCCs of the states (can be NULL).
allowed	Array of booleans indexed by the states. If allowed[q] is true, the state q is allowed to be a root of a tree in the spanning forest. Can be NULL, in which case all states are allowed to be roots of the trees in the spanning forest. Only considered when sccs is not NULL.

◆ decid_grp_sep()

bool decid_grp_sep	(	nfa *	I1,
		nfa *	I2,
		bool	details,
		FILE *	out )

GR-separation.

Remarks: Results of the computation are displayed on a stream given in parameter. A NULL pointer should be given if no display is wanted. It is possible to ask for details on the computation using the Boolean.

Returns: A Boolean indicating whether the two input languages are GR-separable.

Parameters

I1	First NFA.
I2	Second NFA.
details	Should further details be displayed?
out	The stream.

◆ decid_mod_sep()

bool decid_mod_sep	(	nfa *	I1,
		nfa *	I2,
		bool	details,
		FILE *	out )

MOD-separation.

Remarks: Results of the computation are displayed on a stream given as input. A NULL pointer should be given if no display is wanted. It is possible to ask for details on the computation using the Boolean.

Returns: A Boolean indicating whether the two input languages are MOD-separable.

Parameters

I1	First NFA.
I2	Second NFA.
details	Should further details be displayed?
out	The stream.

◆ decid_st_sep()

bool decid_st_sep	(	nfa *	I1,
		nfa *	I2,
		FILE *	out )

ST-separation.

Remarks: Results of the computation are displayed on a stream given as input. A NULL pointer should be given if no display is wanted.

Returns: A Boolean indicating whether the two input languages are ST-separable.

Parameters

I1	First NFA.
I2	Second NFA.
out	The stream.

◆ delete_span_forest()

void delete_span_forest ( num_span_forest * forest )

Deletes the structure used to store the spanning forest.

Parameters

forest The structure to delete.

◆ dfa_compute_folding()

dfa * dfa_compute_folding	(	dfa *	A,
		basis	ba )

Parameters

A	The DFA to fold.
ba	The basis mode (ST, MOD, AMT or GR).

◆ dgraph_amt_fold()

parti * dgraph_amt_fold	(	dgraph *	g,
		parti *	sccs )

Computes the folding of a dgraph according to the AMT-separation.

Remarks: The partition into sccs is not mandatory. If a NULL pointer is given, it is assumed that the dgraph consists of a single SCC (if this is not the case, the result is undefined).

Parameters

g	The dgraph to fold.
sccs	The partition into SCCs of the states (can be NULL).

◆ dgraph_implement_fold()

dgraph * dgraph_implement_fold	(	dgraph *	g,
		parti *	sccs,
		parti *	fold )

Folds a single SCC of a dgraph according to a folding partition generated from MOD, AMT or GR.

Remarks: The sccs are not mandatory. If a NULL pointer is given, it is assumed that the dgraph contain no edge outside of the SCCs (if this is not the case, the result is undefined). If the sccs are given, the edges outside of the SCCs are not copied to the folded graph.

Returns: The folded graph.

Parameters

g	The dgraph to fold.
sccs	The partition into SCCs of the states.
fold	The partition to use for the fold.

◆ dgraph_stal_fold()

parti * dgraph_stal_fold	(	dgraph *	G,
		parti *	sccs,
		basis	ba )

Computes the Stalling partition obtained from a dgraph.

Remarks: In group mode, the alphabet is preserved, in modulo mode, it is reduced to a single letter.; The partition into sccs is not mandatory. If a NULL pointer is given, it is assumed that all existing transitions are internal to the SCCs (if not, the result is undefined). A transition is non-existent if its outgoing edge is UINT_MAX.

Returns: The partition.

Parameters

G	The graph to fold.
sccs	The partition into SCCs of the states.
ba	The basis mode (ST, MOD, AMT or GR).

◆ nfa_dyck_ext()

nfa * nfa_dyck_ext	(	nfa *	A,
		parti *	FOLD )

Computation of the NFA used in the group separation algorithm by adding epsilon transitions between pairs of states connected by a word in the Dyck language.

Attention: Inverse transitions must already be computed.

Returns: The NFA.

Parameters

A	The NFA (inverse transitions must be computed).
FOLD	The partition corresponding to the folding of the SCCs.

◆ nfa_inv_ext()

parti * nfa_inv_ext ( nfa * A )

Computation of the inverse transitions inside the SCCs of an NFA.

Remarks: If there are already inverse transitions, they are deleted and computed again. Epsilon transitions are eliminated before the computation.

Returns: The partition into SCCs used for the computation (it is often useful for further computations).

Parameters

A The NFA.

◆ nfa_proj_unary()

nfa * nfa_proj_unary ( nfa * A )

Projection of a NFA over a one-letter alphabet.

Returns: The projection.

Parameters

A The NFA.

◆ nfa_remove_inv()

void nfa_remove_inv ( nfa * A )

Remove all inverse transitions in an NFA.

Parameters

A The NFA.

◆ nfa_stal_fold()

parti * nfa_stal_fold	(	nfa *	A,
		parti *	sccs )

Computation of the partition obtained by the Stallings folding in SCCs.

Attention: Inverse transitions must be already computed.

Returns: The partition.

Parameters

A	The NFA (inverse transitions must be computed).
sccs	The partition into SCCs of the states.

◆ shrink_grp()

dgraph * shrink_grp	(	dgraph *	g,
		parti *	fold,
		parti *	sccs )

Computes the graph obtained by folding a right or left Cayley graph according to the Stalling partition. Group mode: the alphabet is preserved.

Remarks: Undefined transitions (which go outside of a SCC) are mapped to UINT_MAX.

Returns: The folded graph.

Parameters

g	The graph to fold (right or left Cayley graph of a morphism).
fold	The stalling partition.
sccs	The partition into SCCs of the states (R-classes or L-classes).

◆ shrink_grp_mirror()

dgraph * shrink_grp_mirror	(	dgraph *	g,
		parti *	fold,
		parti *	sccs )

Computes the graph obtained by folding a right or left Cayley graph according to the Stalling partition. Group mode: the alphabet is preserved. Mirror mode: the transitions are reversed.

Remarks: Undefined transitions (which go outside of a SCC) are mapped to UINT_MAX.

Returns: The folded graph.

Parameters

g	The graph to fold (right or left Cayley graph of a morphism).
fold	The stalling partition.
sccs	The partition into SCCs of the states (R-classes or L-classes).

◆ shrink_mod()

dgraph * shrink_mod	(	dgraph *	g,
		parti *	fold,
		parti *	sccs )

Computes the graph obtained by folding a right or left Cayley graph according to the Stalling partition. Modulo mode: the alphabet is reduced to a single letter.

Remarks: Undefined transitions (which go outside of a SCC) are mapped to UINT_MAX.

Returns: The folded graph.

Parameters

g	The graph to fold (right or left Cayley graph of a morphism).
fold	The stalling partition.
sccs	The partition into SCCs of the states (R-classes or L-classes).

◆ shrink_mod_mirror()

dgraph * shrink_mod_mirror	(	dgraph *	g,
		parti *	fold,
		parti *	sccs )

Computes the graph obtained by folding a right or left Cayley graph according to the Stalling partition. Modulo mode: the alphabet is reduced to a single letter. Mirror mode: the transitions are reversed.

Remarks: Undefined transitions (which go outside of a SCC) are mapped to UINT_MAX.

Returns: The folded graph.

Parameters

g	The graph to fold (right or left Cayley graph of a morphism).
fold	The stalling partition.
sccs	The partition into SCCs of the states (R-classes or L-classes).

Classes

Functions

Detailed Description

Function Documentation

◆ compute_amt_kernel_regular()

◆ compute_amt_pairs_regular()

◆ compute_span_forest()

◆ decid_grp_sep()

◆ decid_mod_sep()

◆ decid_st_sep()

◆ delete_span_forest()

◆ dfa_compute_folding()

◆ dgraph_amt_fold()

◆ dgraph_implement_fold()

◆ dgraph_stal_fold()

◆ nfa_dyck_ext()

◆ nfa_inv_ext()

◆ nfa_proj_unary()

◆ nfa_remove_inv()

◆ nfa_stal_fold()

◆ shrink_grp()

◆ shrink_grp_mirror()

◆ shrink_mod()

◆ shrink_mod_mirror()