Data Structures
struct	sataf_msa_info
	Data structure gathering quantitative informations related to a MSA. This structure is filled by the function sataf_msa_get_info. More...

Macros
#define	sataf_msa_empty sataf_msa_zero
	Alias for the sataf_msa_zero function.

#define	sataf_msa_all sataf_msa_one
	Alias for the sataf_msa_one function.

Typedefs
typedef struct sataf_msa_st	sataf_msa
	Type for the data structure encoding Marked Shared Automata.

Functions
sataf_msa *	sataf_msa_find_or_add (sataf_sa *sa, uint32_t initial)
	Getting the unique MSA defined by the couple (sa,initial). More...

static uint32_t	sataf_msa_get_state (sataf_msa *msa)
	Return the marked state defining msa. More...

static sataf_sa *	sataf_msa_get_sa (sataf_msa *msa)
	Return the shared automaton defining msa. More...

static sataf_sa *	sataf_msa_get_sa_no_ref (sataf_msa *msa)
	Return the shared automaton defining msa but without incrementing its counter of references. More...

static sataf_msa *	sataf_msa_compute (sataf_mao *A)
	Minimize, canonicalize and share the given MAO A. More...

sataf_msa *	sataf_msa_compute_with_transformer (sataf_mao A, sataf_sa_transformer T)
	Minimize, canonicalize and share the given MAO A. More...

sataf_mao *	sataf_msa_to_mao (sataf_msa *msa)
	Create a MAO from msa. More...

void	sataf_msa_log_info (ccl_log_type log, sataf_msa *msa)
	Display on log quantitative informations about the structure of msa. More...

void	sataf_msa_get_info (sataf_msa msa, sataf_msa_info info)
	Retrieve quantitative informations related to msa. More...

sataf_msa *	sataf_msa_succ (sataf_msa *msa, uint32_t a)
	Return the successor of msa by the letter a. More...

static int	sataf_msa_is_final (sataf_msa *msa)
	Return if msa accepts the empty word. More...

static uint32_t	sataf_msa_get_alphabet_size (sataf_msa *msa)
	Return the size of the alphabet. More...

static sataf_msa *	sataf_msa_add_reference (sataf_msa *msa)
	Increment the counter of references of msa. More...

static void	sataf_msa_del_reference (sataf_msa *msa)
	Decrement the counter of references of msa. More...

void	sataf_msa_display_as_dot (sataf_msa msa, ccl_log_type log, const char *alphabet, int with_info)
	Display the given MSA into the DOT file format. More...

void	sataf_msa_display_as_olddot (sataf_msa msa, ccl_log_type log, const char *alphabet)
	Another function used to display the given MSA into the DOT file format. More...

static int	sataf_msa_is_zero (sataf_msa *msa)
	Check if msa is the one recognizing nothing. More...

static int	sataf_msa_is_one (sataf_msa *msa)
	Check if msa is the one recognizing everything. More...

static int	sataf_msa_is_zero_or_one (sataf_msa *msa)
	Check if msa is one of the two elementary MSAs i.e. either the one recognizing everything or the one recognizing nothing. More...

int	sataf_msa_is_included_in (sataf_msa a1, sataf_msa a2)
	Check the inclusion of $L_{a_1}$ in $L_{a_2}$ . More...

sataf_msa *	sataf_msa_zero (uint32_t alphabet_size)
	Return the empty language. More...

sataf_msa *	sataf_msa_one (uint32_t alphabet_size)
	Compute $\Sigma^\star$ . More...

sataf_msa *	sataf_msa_epsilon (uint32_t alphabet_size)
	Create the singleton containing the empty word. More...

sataf_msa *	sataf_msa_letter (uint32_t alphabet_size, uint32_t a)
	Create the singleton containing the letter a. More...

sataf_msa *	sataf_msa_alphabet (uint32_t alphabet_size)
	Create the language equal to the alphabet of size alphabet_size. More...

sataf_msa *	sataf_msa_ite (sataf_msa i, sataf_msa t, sataf_msa *e)
	Boolean operation : if-then-else. More...

sataf_msa *	sataf_msa_not (sataf_msa *a)
	Boolean operation : complement. More...

sataf_msa *	sataf_msa_or (sataf_msa a1, sataf_msa a2)
	Boolean operation : disjunction. More...

sataf_msa *	sataf_msa_xor (sataf_msa a1, sataf_msa a2)
	Boolean operation : mutual exclusion. More...

sataf_msa *	sataf_msa_and (sataf_msa a1, sataf_msa a2)
	Boolean operation : conjunction. More...

sataf_msa *	sataf_msa_imply (sataf_msa a1, sataf_msa a2)
	Boolean operation : implication. More...

sataf_msa *	sataf_msa_equiv (sataf_msa a1, sataf_msa a2)
	Boolean operation : equivalence. More...

sataf_msa *	sataf_msa_forall (sataf_msa *a)
	Create the MSA encoding the intersection of residues of . More...

sataf_msa *	sataf_msa_exists (sataf_msa *a)
	Create the MSA encoding the union of residues of . More...

sataf_msa *	sataf_msa_concat (sataf_msa a1, sataf_msa a2)
	Concatenation of $L_{a_1}$ and $L_{a_2}$ . More...

sataf_msa *	sataf_msa_power (sataf_msa *a, int N)
	Exponentiation of . More...

sataf_msa *	sataf_msa_star (sataf_msa *a)
	Transitive closure of . More...

int	sataf_msa_is_detectable (sataf_msa a1, sataf_msa a2, ccl_list *acc)
	check if a1 is detectable in a2 More...

sataf_msa *	sataf_msa_cache_get (sataf_msa a1, sataf_msa a2, sataf_msa a3, const void aux)
	Look for a result in the cache over MSA operations. More...

void	sataf_msa_cache_put (sataf_msa a1, sataf_msa a2, sataf_msa a3, const void aux, sataf_msa *R)
	Add en entry into the cache for MSA operations. More...

Detailed Description

Function Documentation

static sataf_msa* sataf_msa_add_reference ( sataf_msa * msa )

inlinestatic

Increment the counter of references of msa.

Parameters

msa	the marked shared automaton

Precondition: msa != NULL

Returns: msa

sataf_msa* sataf_msa_alphabet ( uint32_t alphabet_size )

Create the language equal to the alphabet of size alphabet_size.

Parameters

alphabet_size the size of the alphabet $\Sigma$

Precondition: alphabet_size > 0

Returns: $\Sigma$ such that $|\Sigma|$ = alphabet_size

sataf_msa* sataf_msa_and	(	sataf_msa *	a1,
		sataf_msa *	a2
	)

Boolean operation : conjunction.

Parameters

a1, a2 the marked shared automata

Precondition: a1 != NULL && a2 != NULL

Returns: the MSA encoding $L_{a_1}\cap L_{a_2}$

sataf_msa* sataf_msa_cache_get	(	sataf_msa *	a1,
		sataf_msa *	a2,
		sataf_msa *	a3,
		const void *	aux
	)

Look for a result in the cache over MSA operations.

This function finds an entry (a1,a2,a3,aux,R) then it returns a new reference to R. aux is a generic pointer which can be used to identify the cached operation (by using, for instance, the address of the function which implements the operation).

Parameters

a1	the first MSA operand of the cached operation
a2	the second MSA but optional operand
a3	the third MSA but optional operand
aux	a generic identifier.

Precondition: a1 != NULL

Returns: the MSA R if the cache contains an entry (a1,a2,a3,aux,R).

void sataf_msa_cache_put	(	sataf_msa *	a1,
		sataf_msa *	a2,
		sataf_msa *	a3,
		const void *	aux,
		sataf_msa *	R
	)

Add en entry into the cache for MSA operations.

This function puts a new record into the cache for MSA operations. The counter of references is incremented for each non-null $a_i$ . The fourth parameter aux is copied as is. The new entry might overwrite an existing one; in this case, the replaced $a_i$ and $R$ are dereferenced.

Parameters

a1	the first MSA operand
a2	the second MSA but optional operand
a3	the third MSA but optional operand
aux	a generic identifier
R	the result of the cached operation

Precondition: a1 != NULL

static sataf_msa* sataf_msa_compute ( sataf_mao * A )

inlinestatic

Minimize, canonicalize and share the given MAO A.

This function is equivalent to sataf_msa_compute_with_transformer (A, NULL).

Parameters

A	the MAO to canonicalize

Precondition: A != NULL

Returns: the unique MSA encoding the same language than A.

sataf_msa* sataf_msa_compute_with_transformer	(	sataf_mao *	A,
		sataf_sa_transformer *	T
	)

Minimize, canonicalize and share the given MAO A.

This is the function transforming a generic automaton given as a MAO into the shared and canonical data structure called MSA.

Prior the call to the minimization algorithm the function T is called with the exit automaton and the binding function used to create the minimal shared component. This function can be used to change the acceptance condition.

Parameters

A	the MAO to canonicalize
T	a transformation function

Precondition: A != NULL

Returns: the unique MSA encoding the language recognized by A.

sataf_msa* sataf_msa_concat	(	sataf_msa *	a1,
		sataf_msa *	a2
	)

Concatenation of $L_{a_1}$ and $L_{a_2}$ .

Parameters

a1, a2 the marked shared automata

Precondition: a1 != NULL && a2 != NULL

Returns: the MSA encoding $L_{a_1}.L_{a_2}$ .

static void sataf_msa_del_reference ( sataf_msa * msa )

inlinestatic

Decrement the counter of references of msa.

When the counter of references of msa falls to zero the resources allocated to it are freed.

Parameters

msa	the marked shared automaton

Precondition: msa != NULL

void sataf_msa_display_as_dot	(	sataf_msa *	msa,
		ccl_log_type	log,
		const char **	alphabet,
		int	with_info
	)

Display the given MSA into the DOT file format.

Parameters

msa	the displayed MSA.
log	the CCL output stream
alphabet	an array of labels used as letters.

Precondition: msa != NULL

See Also: http://www.graphviz.org

void sataf_msa_display_as_olddot	(	sataf_msa *	msa,
		ccl_log_type	log,
		const char **	alphabet
	)

Another function used to display the given MSA into the DOT file format.

Parameters

msa	the displayed MSA.
log	the CCL output stream
alphabet	an array of labels used as letters.

Precondition: msa != NULL

See Also: http://www.graphviz.org

sataf_msa* sataf_msa_epsilon ( uint32_t alphabet_size )

Create the singleton containing the empty word.

Parameters

alphabet_size the size of the alphabet $\Sigma$

Precondition: alphabet_size > 0

Returns: $\{\epsilon\}$

sataf_msa* sataf_msa_equiv	(	sataf_msa *	a1,
		sataf_msa *	a2
	)

Boolean operation : equivalence.

Parameters

a1, a2 the marked shared automata

Precondition: a1 != NULL && a2 != NULL

Returns: the MSA encoding $\overline{L_{a_1}}\cap \overline{L_{a_2}}\cup L_{a_1}\cap L_{a_2}$

sataf_msa* sataf_msa_exists ( sataf_msa * a )

Create the MSA encoding the union of residues of $L_a$ .

Parameters

a	the MAO argument

Precondition: a != NULL

Returns: the MSA encoding $\bigcup_{\alpha\in \Sigma} \alpha^{-1}L_a$

sataf_msa* sataf_msa_find_or_add	(	sataf_sa *	sa,
		uint32_t	initial
	)

Getting the unique MSA defined by the couple (sa,initial).

This function looks up in the unicity table of MSAs for the one defined by (sa, initial). The state initial must be a valid state of the strongly connected component defining sa.

Parameters

sa	the shared automaton defining the result.
initial	the state to mark in sa

Precondition: sa != NULL

Returns: MSA(sa, initial).

sataf_msa* sataf_msa_forall ( sataf_msa * a )

Create the MSA encoding the intersection of residues of $L_a$ .

Parameters

a	the MAO argument

Precondition: a != NULL

Returns: the MSA encoding $\bigcap_{\alpha\in \Sigma} \alpha^{-1}L_a$

static uint32_t sataf_msa_get_alphabet_size ( sataf_msa * msa )

inlinestatic

Return the size of the alphabet.

Parameters

msa	the considered marked shared automaton

Precondition: msa != NULL

Returns: the size of the underlying alphabet

void sataf_msa_get_info	(	sataf_msa *	msa,
		sataf_msa_info *	info
	)

Retrieve quantitative informations related to msa.

This function fills the structure pointed by info.

Parameters

msa	the considered MSA
info	structure receiving values

Precondition: msa != NULL && info != NULL

static sataf_sa* sataf_msa_get_sa ( sataf_msa * msa )

inlinestatic

Return the shared automaton defining msa.

Parameters

msa	the considered MSA

Precondition: msa != NULL

Returns: the shared automaton defining msa.

static sataf_sa* sataf_msa_get_sa_no_ref ( sataf_msa * msa )

inlinestatic

Return the shared automaton defining msa but without incrementing its counter of references.

Parameters

msa	the considered MSA

Precondition: msa != NULL

Returns: the shared automaton defining msa.

static uint32_t sataf_msa_get_state ( sataf_msa * msa )

inlinestatic

Return the marked state defining msa.

Parameters

msa	the considered MSA

Precondition: msa != NULL

Returns: the marked state defining msa.

sataf_msa* sataf_msa_imply	(	sataf_msa *	a1,
		sataf_msa *	a2
	)

Boolean operation : implication.

Parameters

a1, a2 the marked shared automata

Precondition: a1 != NULL && a2 != NULL

Returns: the MSA encoding $\overline{L_{a_1}}\cup L_{a_2}$

int sataf_msa_is_detectable	(	sataf_msa *	a1,
		sataf_msa *	a2,
		ccl_list *	acc
	)

check if a1 is detectable in a2

This function checks if a1 is detectable in a2 i.e. if it is possible to change the acceptance condition of a2 in such a way that the obtained automaton recognize the same language than a1.

Parameters

a1	automaton for which the detectability is checked
a2	second operand
acc	the list of states of a2 that have to accepting in order to obtain a2

Precondition: a1 != NULL; a2 != NULL

Returns: a non null value if a1 is detectable in a2.

static int sataf_msa_is_final ( sataf_msa * msa )

inlinestatic

Return if msa accepts the empty word.

This function checks if the state of the automaton underlying to msa is accepting or not.

Parameters

msa	the considered MSA

Precondition: msa != NULL

Returns: a non-null value if msa accepts $\epsilon$ .

int sataf_msa_is_included_in	(	sataf_msa *	a1,
		sataf_msa *	a2
	)

Check the inclusion of $L_{a_1}$ in $L_{a_2}$ .

Parameters

a1, a2 the marked shared automata

Precondition: a1 != NULL && a2 != NULL

Returns: a non-null value iff $L_{a_1}\subseteq L_{a_2}$ .

static int sataf_msa_is_one ( sataf_msa * msa )

inlinestatic

Check if msa is the one recognizing everything.

Parameters

msa	the marked shared automaton

Precondition: msa != NULL

Returns: a non-null value if msa recognizes all words.

static int sataf_msa_is_zero ( sataf_msa * msa )

inlinestatic

Check if msa is the one recognizing nothing.

Parameters

msa	the marked shared automaton

Precondition: msa != NULL

Returns: a non-null value if msa recognizes no word.

static int sataf_msa_is_zero_or_one ( sataf_msa * msa )

inlinestatic

Check if msa is one of the two elementary MSAs i.e. either the one recognizing everything or the one recognizing nothing.

Parameters

msa	the marked shared automaton

Precondition: msa != NULL

Returns: sataf_msa_is_one (msa) || sataf_msa_is_zero (msa)

sataf_msa* sataf_msa_ite	(	sataf_msa *	i,
		sataf_msa *	t,
		sataf_msa *	e
	)

Boolean operation : if-then-else.

Parameters

i	the if MSA operand
t	the then MSA operand
e	the else MSA operand

Precondition: a1 != NULL && a2 != NULL && a3 != NULL

Returns: the MSA encoding $L_{a_1}\cap L_{a_2}\cup \overline{L_{a_1}}\cap L_{a_3}$

sataf_msa* sataf_msa_letter	(	uint32_t	alphabet_size,
		uint32_t	a
	)

Create the singleton containing the letter a.

Parameters

alphabet_size	the size of the alphabet $\Sigma$
a	the letter

Precondition: alphabet_size > 0; a < alphabet_size

Returns: $\{a\}$

void sataf_msa_log_info	(	ccl_log_type	log,
		sataf_msa *	msa
	)

Display on log quantitative informations about the structure of msa.

Parameters

msa	the considered MSA
log	the CCL output stream

Precondition: msa != NULL

sataf_msa* sataf_msa_not ( sataf_msa * a )

Boolean operation : complement.

Parameters

a	the marked shared automata

Precondition: a != NULL

Returns: the MSA encoding $\Sigma^\star\setminus L_a$

sataf_msa* sataf_msa_one ( uint32_t alphabet_size )

Compute $\Sigma^\star$ .

Parameters

alphabet_size the size of the alphabet $\Sigma$

Precondition: alphabet_size > 0

Returns: the msa encoding $\Sigma^\star$ with $|\Sigma|$ =alphabet_size

sataf_msa* sataf_msa_or	(	sataf_msa *	a1,
		sataf_msa *	a2
	)

Boolean operation : disjunction.

Parameters

a1, a2 the marked shared automata

Precondition: a1 != NULL && a2 != NULL

Returns: the MSA encoding $L_{a_1}\cup L_{a_2}$

sataf_msa* sataf_msa_power	(	sataf_msa *	a,
		int	N
	)

Exponentiation of $L_a$ .

Parameters

a	the marked shared automaton
N	the exponent

Precondition: a != NULL; N >= 0

Returns: the MSA encoding

sataf_msa* sataf_msa_star ( sataf_msa * a )

Transitive closure of $L_a$ .

Parameters

a	the marked shared automaton

Precondition: a != NULL

Returns: the MSA encoding

sataf_msa* sataf_msa_succ	(	sataf_msa *	msa,
		uint32_t	a
	)

Return the successor of msa by the letter a.

Parameters

msa	the considered MSA
a	the letter

Precondition: msa != NULL; a < sataf_msa_get_alphabet_size (msa)

Returns: the successor MSA of msa by a

sataf_mao* sataf_msa_to_mao ( sataf_msa * msa )

Create a MAO from msa.

Parameters

msa	the considered MSA

Precondition: msa != NULL

Returns: a MAO having the same behaviors then msa

sataf_msa* sataf_msa_xor	(	sataf_msa *	a1,
		sataf_msa *	a2
	)

Boolean operation : mutual exclusion.

Parameters

a1, a2 the marked shared automata

Precondition: a1 != NULL && a2 != NULL

Returns: the MSA encoding $L_{a_1}\oplus L_{a_2}$

sataf_msa* sataf_msa_zero ( uint32_t alphabet_size )

Return the empty language.

Parameters

alphabet_size the size of the reference alphabet

Precondition: alphabet_size > 0

Returns: the empty language $\emptyset\subset\Sigma^\star$ for an alphabet $\Sigma$ of size alphabet_size.

Data Structures

Macros

Typedefs

Functions

Detailed Description

Function Documentation